Boosting MCSat modulo nonlinear integer arithmetic via local search

DOI10.1007/978-3-031-99984-0_6MaRDI QIDQ6869961zbMATH OpenFDO

Authors Enrico Lipparini, Thomas Hader, Ahmed Irfan, Stéphane Graham-Lengrand

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_6

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• A model-constructing satisfiability calculus
• Better Decision Heuristics in CDCL through Local Search and Target Phases
• Deep cooperation of CDCL and local search for SAT
• Experimenting on solving nonlinear integer arithmetic with incremental linearization
• Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 545277 (Why is no real title available?)
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Local search for solving satisfiability of polynomial formulas
• Local Search for Unsatisfiability
• Local Search for SMT on Linear Integer Arithmetic
• MCSat-based finite field reasoning in the \textsc{Yices2} SMT solver (short paper)
• Modular strategic SMT solving with \textbf{SMT-RAT}
• Propagation based local search for bit-precise reasoning
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Satisfiability of non-linear transcendental arithmetic as a certificate search problem
• SMT solving over finite field arithmetic
• Solving bitvectors with MCSAT: explanations from bits and pieces
• Solving nonlinear integer arithmetic with MCSAT
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Stochastic local search for SMT: combining theory solvers with WalkSAT
• The MathSAT5 SMT solver

This page was built for publication: Boosting MCSat modulo nonlinear integer arithmetic via local search

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6869961)