@CONFERENCE\{IMM2003-02531,
    author       = "M. Fr{\"{a}}nzle and C. Herde",
    title        = "Efficient {SAT} engines for concise logics: Accelerating proof search for zero-one linear constraint systems",
    year         = "2003",
    month        = "sep",
    keywords     = "Satisfiability; non-clausal propositional logic;
 zero-one linear constraint systems; proof search; acceleration techniques",
    pages        = "302-316",
    booktitle    = "Logic for Programming, Artificial Intelligence and Reasoning ({LPAR} 2003)",
    volume       = "2850",
    series       = "{LNCS,} subseries {LNAI}",
    editor       = "Moshe Y. Vardi, Andrei Voronkov",
    publisher    = "Springer Verlag",
    organization = "",
    address      = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/2531-full.html",
    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."
}