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

Martin Fränzle, Christian Herde

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    1 Downloads (Pure)

    Abstract

    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.
    Original languageEnglish
    Title of host publicationLogic for Programming, Artificial Intelligence and Reasoning (LPAR 2003)
    Place of PublicationNew York
    PublisherSpringer
    Publication date2003
    Pages302-316
    ISBN (Print)35-40-20101-7
    DOIs
    Publication statusPublished - 2003
    EventLPAR 2003 - Almaty, Kazakhstan
    Duration: 1 Jan 2003 → …
    Conference number: 10

    Conference

    ConferenceLPAR 2003
    Number10
    CityAlmaty, Kazakhstan
    Period01/01/2003 → …

    Keywords

    • zero-one linear constraint systems
    • proof search
    • non-clausal propositional logic
    • acceleration techniques
    • Satisfiability

    Cite this