Improving NLSAT for Nonlinear Real Arithmetic

TL;DR

This paper enhances NLSAT for nonlinear real arithmetic by integrating clause-level information into decision-making, leading to a more efficient solver that outperforms existing SMT solvers on satisfiable instances.

Contribution

It introduces two novel algorithmic improvements—feasible-set-based look-ahead and arithmetic propagation heuristics—and implements them in clauseSMT, improving performance on nonlinear real arithmetic problems.

Findings

clauseSMT outperforms existing SMT solvers on satisfiable SMT(QF_NRA) instances

The proposed methods reduce unnecessary conflicts and improve decision efficiency

Experimental results demonstrate the effectiveness of clause-level information integration

Abstract

The Model-Constructing Satisfiability Calculus (MCSAT) framework has been applied to SMT problems over various arithmetic theories. NLSAT, an implementation using cylindrical algebraic decomposition (CAD) for explanation, is especially competitive for nonlinear real arithmetic (NRA) constraints. However, current Conflict-Driven Clause Learning (CDCL)-style algorithms only consider literal information when making decisions, and thus ignore the influence of clauses on arithmetic variables. This limitation may lead NLSAT to encounter unnecessary conflicts due to suboptimal literal choices. To address this issue, we analyze conflicts caused by literal decisions and incorporate clause-level information that directly affects arithmetic variables. We propose two main algorithmic improvements: a clause-level feasible-set-based look-ahead mechanism and an arithmetic propagation-based branching heuristic. We implement our solver, named clauseSMT, based on a dynamic variable ordering framework. Experiments indicate that clauseSMT is competitive on nonlinear real arithmetic problems compared with existing SMT solvers (CVC5, Z3, YICES2), and it outperforms all of them on satisfiable instances of SMT(QF_NRA) in SMT-LIB. We also evaluate the effectiveness of our proposed methods.