Efficient SAT engines for concise logics: Accelerating proof search for zero-one linear constraint systems



AbstractWe 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.
KeywordsSatisfiability; non-clausal propositional logic; zero-one linear constraint systems; proof search; acceleration techniques
TypeConference paper [With referee]
ConferenceLogic for Programming, Artificial Intelligence and Reasoning (LPAR 2003)
EditorsMoshe Y. Vardi, Andrei Voronkov
Year2003    Month September    Vol. 2850    pp. 302-316
PublisherSpringer Verlag
SeriesLNCS, subseries LNAI
Electronic version(s)[ps]
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering