Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

By Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. 2006

992 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Computer Networks and Communications

Citations in the corpus

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017, methodology): “Given a theory T with signature Σ, the DPLL(T ) architecture [27] provides a generic approach for determining the T -satisfiability of Σ-formulas.”
Multi-shot ASP solving with clingo (2017, methodology): “Given this, dlvhex can be seen as an ASP modulo Theory solver, similar to SAT modulo Theory solvers (Nieuwenhuis et al. 2006).”
Handbook of satisfiability (2009, methodology): “6 More recent and richer formal frameworks for representing DPLL and DPLL-based procedures are described in [73, 54].”
ManySAT: a Parallel SAT Solver (2009, methodology): “One domain which particularly benefits from the recent advances in SAT is Satisfiability Modulo Theory [ 32 ].”
Challenging SMT solvers to verify neural networks (2012, positive): “Satisﬁability Modulo Theory (SMT) can be traced back to seminal work of Nelson and Oppen – see, e.g., [29] – and has enjoyed a growing interest over the recent years – see, e.g., [1,3,4,30], to cite only some of the most relevant contributions.”
Potassco: The Potsdam Answer Set Solving Collection (2011, positive): “clingcon follows the so-called lazy approach of advanced SMT solvers by abstracting from the constraints in a specialized theory [85].”
Satisfiability modulo counting: a new approach for analyzing privacy properties (2014, background): “(Rational polyhedron).”
Solving non-linear arithmetic (2012, methodology): “We describe our procedure as an abstract transition system in the spirit of Abstract DPLL [37,29].”
Handbook of Satisfiability (2021, methodology): “As with early-pruning, there are different strategies by which T -propagation can be interleaved with unitpropagation [4, 8, 72, 34, 111, 49, 114].”
Automated Planning and Acting (2016, methodology): “[246] use a “planning modulo theories” approach that builds on recent work on SAT modulo theories [456, 41].”
Lazy proofs for DPLL(T)-based SMT solvers (2016, methodology): “We assume (as in [21]) that each Ti-solver provides an explaini method with the property that if l is a”
Answer Set Solving in Practice (2012, neutral): “[66] R.”
Conflict-driven answer set solving: From theory to practice (2012, background): “[104]) to concepts available in extended logic programs [119], viz.”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, methodology): “The Propositional Engine serves as the core CDCL( T ) engine [99], which takes the Boolean abstraction of the input formula (together with any lemmas produced during solving) and produces a satisfying assignment for that abstraction.”
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, methodology): “The implementation of CVC4 is a refinement of Abstract DPLL(T) [90].”