An abstract interpretation of DPLL(T)

DOI10.1007/978-3-642-35873-9_27MaRDI QIDQ2926657zbMATH OpenOpenAlexFDO

Authors Martin Brain, Vijay D'Silva, Leopold Haller, Alberto Griggio, Daniel Kroening

Publication date 3 November 2014

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

Full work available at URL https://doi.org/10.1007/978-3-642-35873-9_27

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Logic for Programming, Artificial Intelligence, and Reasoning
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Engineering DPLL(T) + Saturation
• Computer Aided Verification
• Computer Aided Verification

Cited in

(9)

• Constructing cycles in the simplex method for DPLL(T)
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• Satisfiability modulo theories
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Natural domain SMT: a preliminary assessment
• Deciding floating-point logic with abstract conflict driven clause learning
• Symbolic execution as DPLL modulo theories
• Splitting on Demand in SAT Modulo Theories
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: An abstract interpretation of DPLL(T)

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