DPLL(T): Fast Decision Procedures
Top Cited Papers
- 1 January 2004
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
Abstract
The logic of equality with uninterpreted functions (EUF) and its extensions have been widely applied to processor verification, by means of a large variety of progressively more sophisticated (lazy or eager) translations into propositional SAT. Here we propose a new approach, namely a general DPLL(X) engine, whose parameter X can be instantiated with a specialized solver Solver T for a given theory T, thus producing a system DPLL(T). We describe this DPLL(T) scheme, the interface between DPLL(X) and Solver T , the architecture of DPLL(X), and our solver for EUF, which includes incremental and backtrackable congruence closure algorithms for dealing with the built-in equality and the integer successor and predecessor symbols. Experiments with a first implementation indicate that our technique already outperforms the previous methods on most benchmarks, and scales up very well.Keywords
This publication has 21 references indexed in Scilit:
- Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessorsJournal of Symbolic Computation, 2003
- Theorem Proving Using Lazy Proof ExplicationLecture Notes in Computer Science, 2003
- Congruence Closure with Integer OffsetsLecture Notes in Computer Science, 2003
- Boolean satisfiability with transitivity constraintsACM Transactions on Computational Logic, 2002
- A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical PropositionsLecture Notes in Computer Science, 2002
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logicACM Transactions on Computational Logic, 2001
- Validity checking for combinations of theories with equalityPublished by Springer Science and Business Media LLC ,1996
- Variations on the Common Subexpression ProblemJournal of the ACM, 1980
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960