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

DOI10.1007/11591191_3zbMATH Open1143.68579OpenAlexW1561147151MaRDI QIDQ5387828FDOQ5387828

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

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

Mathematics Subject Classification ID

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

Cited In (6)

• Flexible proof production in an industrial-strength SMT solver
• EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas
• BarcelogicTools
• Labelled splitting
• Conflict Resolution
• Combining equational reasoning

Uses Software

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

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)