Proof-generated, BDD-based SAT solver

The program(s) here implement a SAT solver based on BDDs. The key feature is that, for unsatisfiable formulas, they also generate proofs of unsatisfiable in Extended Resolution.

Some inspirations for this work include:

C. Sinz and A. Biere, "Extended resolution proofs for conjoining BDDs," CSR, 2006.

T. Jussila, C. Sinz and A. Biere, "Extended resolution proofs for symbolic SAT solving with quantification," SAT, 2006

J. Franco, M. Kouril, J. Schlipf, J. Ward, S. Weaver, M. Dransfeld, and W. Fleet "SBSAT: a state-based, BDD-based satisfiability solver," SAT 2003

That is, the overall program operation is similar to that of SBSAT, but it generates proofs using generalizations of the ideas found in EBDDRES (Jussila, Sinz, Biere).

Directories:

benchmarks: Contains benchmarks used for evaluting solver

booleforce-1.3: Downloaded from JKU Linz. Make use of its proof checker tracecheck

explore: Code for generating different graph types.

lrat: LRAT proof checker

pcaas: LRAT proof checker modified to support "Proof checking as a service"

protoA: Initial implementation of solver. Uses general-purpose resolution engine

prototype: Refined implementation of solver. Uses resolution engine tailored to needs of solver