作者:
Nieuwenhuis， R.， Oliveras， A. and Tinelli， C.
关键词:
SAT solvers； Satisfiability Modulo Theories
摘要:
We first introduce Abstract DPLL, a rule-based formulation of the Davis-Putnam-LogemannLoveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one
to cleanly express practical DPLL algorithms and to formally reason about them in a simple way.
Its properties, such as soundness, completeness or termination, immediately carry over to the
modern DPLL implementations with features such as backjumping or clause learning.
We then extend the framework to Satisfiability Modulo background Theories (SMT) and use
it to model several variants of the so-called lazy approach for SMT. In particular, we use it to
introduce a few variants of a new, efficient and modular approach for SMT based on a general
DPLL(X) engine, whose parameter X can be instantiated with a specialized solver SolverT for a
given theory T, thus producing a DPLL(T) system. We describe the high-level design of DPLL(X)
and its cooperation with SolverT , discuss the role of theory propagation, and describe different
DPLL(T) strategies for some theories arising in industrial applications.
Our extensive experimental evidence, summarized in this paper, shows that DPLL(T) systems
can significantly outperform the other state-of-the-art tools, frequently even in orders of magnitude, and have better scaling properties.
在线下载