From Propositional Satisfiability to Satisfiability Modulo Theories

DOI10.1007/11814948_1MaRDI QIDQ5756564zbMATH OpenOpenAlexFDO

Authors Hossein M. Sheini, Karem A. Sakallah

Publication date 4 September 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11814948_1

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• A survey of satisfiability modulo theory
• Satisfiability modulo theories
• Formal Methods for Hardware Verification
• Computer Aided Verification
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)

Cited in

(32)

• A framework for satisfiability modulo theories
• Solving quantified verification conditions using satisfiability modulo theories
• Theory decision by decomposition
• Conflict-driven satisfiability for theory combination: transition system and completeness
• SPASS-SATT. A CDCL(LA) solver
• Satisfiability modulo theories and assignments
• Combining SAT methods with non-clausal decision heuristics
• SAT and SMT are still resolution: questions and challenges
• Stochastic local search for SMT: combining theory solvers with WalkSAT
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Engineering DPLL(T) + Saturation
• scientific article; zbMATH DE number 5770428 (Why is no real title available?)
• Instantiation of SMT problems modulo integers
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Satisfiability versus Finite Satisfiability in Elementary Modal Logics
• scientific article; zbMATH DE number 1903356 (Why is no real title available?)
• scientific article; zbMATH DE number 2090300 (Why is no real title available?)
• Solving constraint satisfaction problems with SAT modulo theories
• Deconstructing <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si1.gif" overflow="scroll"><mml:mi mathvariant="script">R</mml:mi><mml:mi mathvariant="sans-serif">eo</mml:mi></mml:math>
• The problem of checking the satisfiability of formulae of decidable theories (survey)
• Modal Satisfiability via SMT Solving
• The MathSAT5 SMT solver
• Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
• Channel-based coordination via constraint satisfaction
• Theory and Applications of Satisfiability Testing
• Mechanizing Mathematical Reasoning
• A Progressive Simplifier for Satisfiability Modulo Theories
• Formal Methods for Hardware Verification
• Reasoning about vectors: satisfiability modulo a theory of sequences
• Optimal rectangle packing
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures

This page was built for publication: From Propositional Satisfiability to Satisfiability Modulo Theories

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