| ||||
| ||||
![]() Title:Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. Conference:CADE-30 Tags:Local Search, MCSat, Nonlinear Integer Arithmetic and SMT 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 Nonlinear Integer Arith- metic (NIA), utilizing accelerated hill-climbing and a new operation called feasible-sets jumping. We implement the proposed approach in the Model Constructing Satisfiability (MCSat) engine of the Yices2 solver, and empirically show its performance using the NIA benchmarks of SMT-LIB. Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. ![]() Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search. | ||||
Copyright © 2002 – 2025 EasyChair |