Local Search for SMT on Linear Integer Arithmetic

DOI10.1007/978-3-031-13188-2_12MaRDI QIDQ6487338zbMATH OpenFDO

Authors Shaowei Cai, Bohan Li, X. D. Zhang

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-13188-2_12

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• A practical approach to satisfiability modulo linear integer arithmetic
• Stochastic local search for SMT: combining theory solvers with WalkSAT
• Precise and complete propagation based local search for satisfiability modulo theories
• Lemma Learning in SMT on Linear Constraints
• Fast cube tests for LIA constraint solving

Cites work

• scientific article; zbMATH DE number 1297592 (Why is no real title available?)
• scientific article; zbMATH DE number 1903346 (Why is no real title available?)
• scientific article; zbMATH DE number 1903355 (Why is no real title available?)
• scientific article; zbMATH DE number 956863 (Why is no real title available?)
• CCAnr: a configuration checking based local search solver for non-random satisfiability
• Choosing probability distributions for stochastic local search and the role of make versus break
• Computer Aided Verification
• Computer Aided Verification
• Computing Stable Models via Reductions to Difference Logic
• Disequality management in integer difference logic via finite instantiations.
• Fast cube tests for LIA constraint solving
• Lazy satisfiability modulo theories
• Local search for Boolean satisfiability with configuration checking and subscore
• Model-driven visualizations of constraint-based local search
• Precise and complete propagation based local search for satisfiability modulo theories
• SPASS-SATT. A CDCL(LA) solver
• Satisfiability modulo theories
• 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
• Stochastic local search. Foundations and applications.
• The MathSAT5 SMT solver
• The small model property: How small can it be?
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(5)

• Stochastic local search for SMT: combining theory solvers with WalkSAT
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Boosting MCSat modulo nonlinear integer arithmetic via local search
• Local-MIP: efficient local search for mixed integer programming
• Local search for solving satisfiability of polynomial formulas

This page was built for publication: Local Search for SMT on Linear Integer Arithmetic

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