Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search

TL;DR

This work addresses the efficiency of solving SMT problems with nonlinear integer arithmetic ($\mathcal{NIA}$) by tightly integrating local search into the MCSat framework. It presents a theory-agnostic approach to guide MCSat decisions using assignments discovered by local search, and develops a specialized LS procedure for $\mathcal{NIA}$ featuring feasible-sets jumping and accelerated hill-climbing. The method is implemented in the Yices2 SMT solver as $\textsc{Yices2}_{LS}$ and evaluated on SMT-LIB $\mathcal{NIA}$ benchmarks, showing improved performance and competitive results against other solvers and portfolios. The results demonstrate reduced conflicts and theory-variable assignments on unsat and sat instances, and highlight the complementary benefits of combining LS with MCSat for both satisfiable and unsatisfiable problems, suggesting broader applicability to additional theories and caching strategies.

Abstract

The Model Constructing Satisfiability (MCSat) approach to the SMT problem extends the ideas of CDCL from the SAT level to the theory level. Like SAT, its search is driven by incrementally constructing a model by assigning concrete values to theory variables and performing theory-level reasoning to learn lemmas when conflicts arise. Therefore, the selection of values can significantly impact the search process and the solver's performance. In this work, we propose guiding the MCSat search by utilizing assignment values discovered through local search. First, we present a theory-agnostic framework to seamlessly integrate local search techniques within the MCSat framework. Then, we highlight how to use the framework to design a search procedure for (quantifier-free) Nonlinear Integer Arithmetic (NIA), utilizing accelerated hill-climbing and a new operation called feasible-sets jumping. We implement the proposed approach in the MCSat engine of the Yices2 solver, and empirically evaluate its performance over the N IA benchmarks of SMT-LIB.

Figures (1)

• Figure 1: The MCSat framework consists of the following steps: 1) Propagate the trail. 2) If a conflict is found during propagation, check if there is any decision to backtrack over. If not, return UNSAT. Otherwise, explain the conflict using a lemma, backtrack the trail, and repeat step 1. 3) If no conflict is found during propagation, decide on a variable that is not on the trail. If there is nothing left to decide, return SAT. Otherwise, add the decided variable to the trail and repeat step 1.