Zhonghan Wang
State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Portfolio: Z3-Plus-Plus in SMT-COMP (NRA Track)

We noticed that the order of variables to be assigned greatly affects the performance on many instances, so we employ different solving flows, mainly including various heuristic arithmetic variable reordering strategies from CAD. Also, as DPLL(T) framework works particularly well for multilinear instances, we extend the time limit of DPLL(T) for such instances. As for NRA theory solving, we implement sample-cell projection in NLSAT explain module. Although the new operator is also a CAD-like projection operator which computes the cell (not necessarily cylindrical) containing a given sample such that each polynomial from the problem is sign-invariant on the cell, it is of singly exponential time complexity. Also we implement a feasible region consistency checker for clauses which are univariate and unit before the main search. The checker obtains the feasible region of variables through real root isolation and continuously takes the intersection of the regions. If the feasible region of some variable becomes empty, it means the instance is unsatisfiable. Otherwise, the obtained feasible regions are added to the instance as lemmas.

Incomplete Method: Local Search for SMT(NRA) Solving

Local search has recently been applied to SMT problems overvarious arithmetic theories. Among these, nonlinear real arithmetic posesspecial challenges due to its uncountable solution space and potentialneed to solve higher-degree polynomials. As a consequence, existing workon local search only considered fragments of the theory. In this work,we analyze the difficulties and propose ways to address them, resultingin an efficient search algorithm that covers the full theory of nonlinearreal arithmetic. In particular, we present two algorithmic improvements:incremental computation of variable scores and temporary relaxation ofequality constraints. We also discuss choice of candidate moves and alook-ahead mechanism in case when no critical moves are available. Theresulting implementation is competitive on satisfiable problem instancesagainst complete methods such as MCSAT in existing SMT solvers.

Complete Method: Improving MCSAT for SMT(NRA) Solving

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.

DNLSAT: A Dynamic Variable Ordering MCSAT Framework for Nonlinear Real Arithmetic
Demonstration Video Code

Satisfiability modulo nonlinear real arithmetic theory (SMT(NRA)) solving is essential to multiple applications, including program verification, program synthesis and software testing. In this context, recently model constructing satisfiability calculus (MCSAT) has been invented to directly search for models in the theory space. Although following papers discussed practical directions and updates on MCSAT, less attention has been paid to the detailed implementation. In this paper, we present an efficient implementation of dynamic variable orderings of MCSAT, called dnlsat.We show carefully designed data structures and promising mechanisms, such as branching heuristic, restart, and lemma management. Besides, we also give a theoretical study of potential influences brought by the dynamic variablr ordering. The experimental evaluation shows that dnlsat accelerates the solving speed and solves more satisfiable instances than other state-of-the-art SMT solvers.