Stochastic local search for SMT: combining theory solvers with WalkSAT

DOI10.1007/978-3-642-24364-6_12MaRDI QIDQ3172891zbMATHOpenAlexFDO

Authors Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi

Publication date 7 October 2011

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL http://qmro.qmul.ac.uk/xmlui/handle/123456789/6099

Mathematics Subject Classification ID

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

Recommendations

• Local Search for SMT on Linear Integer Arithmetic
• Efficient theory combination via Boolean search
• From Propositional Satisfiability to Satisfiability Modulo Theories
• Satisfiability modulo theories
• A survey of satisfiability modulo theory

Cites work

• scientific article; zbMATH DE number 2090300 (Why is no real title available?)
• scientific article; zbMATH DE number 956863 (Why is no real title available?)
• Boosting local search thanks to \textsc{cdcl}
• Fast and Flexible Difference Constraint Propagation for DPLL(T)
• Lazy satisfiability modulo theories
• Local search algorithms for SAT: an empirical evaluation
• Mechanizing Mathematical Reasoning
• Minimizing conflicts: A heuristic repair method for constraint satisfaction and scheduling problems
• Theory and Applications of Satisfiability Testing

Cited in

(6)

• Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic
• Propagation based local search for bit-precise reasoning
• Local search for solving satisfiability of polynomial formulas
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• Local Search for SMT on Linear Integer Arithmetic
• Structured learning modulo theories

Describes a project that uses

Uses Software

• UBCSAT
• MathSAT

This page was built for publication: Stochastic local search for SMT: combining theory solvers with WalkSAT

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