DPLL( T): Fast Decision Procedures

By H. Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. International Conference on Computer Aided Verification, 2004

382 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/9f8d74bef142969c9c1ff2cef2e48a68459f34f1

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

Citations in the corpus

The YICES SMT Solver (2006, background): “The latter are allowed to dynamically create literals and add clauses during the DPLL search, and to send explanations to the SAT solver when they detect inconsistencies or propagate implied literals (see [7,3]).”
SCIP: solving constraint integer programs (2009, background): “To remedy this situation, word level solvers have been proposed [35,47,52,89,101] that address the property checking problem at a higher representation level, the register transfer (RT) level, and try to exploit the structural information therein.”
A Decision Procedure for Bit-Vectors and Arrays (2007, methodology): “STP’s architecture differs significantly from many other decision procedures based on case splitting and backtracking, including tools like SVC, and CVC Lite [3,2], and other solvers based on the Davis-Putnam-Logemann-Loveland (DPLL(T)) architecture [11].”
A Fast Linear-Arithmetic Solver for DPLL(T) (2006, methodology): “1 This is similar to the API proposed in [1].”
Efficient E-Matching for SMT Solvers (2007, positive): “SMT solvers based on a DPLL(T) [1] framework have proven highly scalable, efficient and suitable for integrating theory reasoning.”
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, background): “The most common architecture for building general purpose SMT solvers is DPLL(T) [11, 54, 90, 99].”
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].”
Splitting on Demand in SAT Modulo Theories (2006, background): “DPLL(T ) is a general SMT architecture for the lazy approach [9].”