Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools

DOI10.1007/11591191_3MaRDI QIDQ5387828zbMATH OpenOpenAlexFDO

Authors Robert Nieuwenhuis, Albert Oliveras

Publication date 27 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11591191_3

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Computer Aided Verification
• Logic for Programming, Artificial Intelligence, and Reasoning
• From Propositional Satisfiability to Satisfiability Modulo Theories
• Challenges in Satisfiability Modulo Theories

Cited in

(6)

• Flexible proof production in an industrial-strength SMT solver
• BarcelogicTools
• EufDPLL -- a tool to check satisfiability of equality logic formulas
• Labelled splitting
• Conflict Resolution
• Combining equational reasoning

Describes a project that uses

Uses Software

• BerkMin
• Chaff
• UCLID
• Siege
• SMT-LIB
• MiniSat

This page was built for publication: Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools

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