Conference paper
Efficient SAT engines for concise logics: Accelerating proof search for zero-one linear constraint systems
We investigate the problem of generalizing acceleration techniques as found in recent satisfiability engines for conjunctive normal forms (CNFs) to linear constraint systems over the Booleans. The rationale behind this research is that rewriting the propositional formulae occurring in e.g. bounded model checking (BMC) [Biere, Cimatti,Zhu, 1999] to CNF requires a blowup in either the formula size (worst-case exponential) or in the number of propositional variables (linear, thus yielding a worst-case exponential blow-up of the search space).
We demonstrate that acceleration techniques like observation lists and lazy clause evaluation [Moskewicz e.a., 2001] as well as the more traditional non-chronological backtracking and learning techniques generalize smoothly to Davis-Putnam-like resolution procedures for the very concise propositional logic of linear constraint systems over the Booleans.
Despite the more expressive input language, the performance of our prototype implementation comes surprisingly close to that of state-of-the-art CNF-SAT engines like ZChaff [Moskewicz e.a., 2001]. First experiments with bounded model-construction problems show that the overhead in the satisfiability engine that can be attributed to the richer input language is often amortized by the conciseness gained in the propositional encoding of the BMC problem.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2003 |
Pages: | 302-316 |
Proceedings: | LPAR 2003 |
ISBN: | 3540201017 , 3540398139 , 9783540201014 and 9783540398134 |
ISSN: | 16113349 and 03029743 |
Types: | Conference paper |
DOI: | 10.1007/b13986 |