Stochastic local search for SMT: combining theory solvers with WalkSAT

DOI10.1007/978-3-642-24364-6_12zbMATH Open1348.68227OpenAlexW1601158010MaRDI QIDQ3172891FDOQ3172891

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

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

Mathematics Subject Classification ID

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

Cites Work

• Theory and Applications of Satisfiability Testing
• Lazy satisfiability modulo theories
• Fast and Flexible Difference Constraint Propagation for DPLL(T)
• Minimizing conflicts: A heuristic repair method for constraint satisfaction and scheduling problems
• Title not available (Why is that?)
• Local search algorithms for SAT: an empirical evaluation
• Mechanizing Mathematical Reasoning
• Title not available (Why is that?)
• Boosting local search thanks to \textsc{cdcl}

Cited In (6)

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

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)