  Model-constructing satisfiability calculus (MCSAT) framework has been applied
to SMT problems on different arithmetic theories. NLSAT, an implementation
using cylindrical algebraic decomposition for explanation, is especially
competitive among nonlinear real arithmetic constraints. However, current
Conflict-Driven Clause Learning (CDCL)-style algorithms only consider literal
information for decision, and thus ignore clause-level influence on arithmetic
variables. As a consequence, NLSAT encounters unnecessary conflicts caused by
improper literal decisions.
  In this work, we analyze the literal decision caused conflicts, and introduce
clause-level information with a direct effect on arithmetic variables. Two main
algorithm improvements are presented: clause-level feasible-set based
look-ahead mechanism and arithmetic propagation based branching heuristic. We
implement our solver named clauseSMT on our dynamic variable ordering
framework. Experiments show that clauseSMT is competitive on nonlinear real
arithmetic theory against existing SMT solvers (cvc5, Z3, Yices2), and
outperforms all these solvers on satisfiable instances of SMT(QF_NRA) in
SMT-LIB. The effectiveness of our proposed methods are also studied.
