This is a BDD based SAT solver that can generate extended resolution proof traces.

New version 1.2 can also solve QBFs and generate certificates. So far, only available in binary.


[ ebddres-1.0.tar.gz | ebddres-1.1.tar.gz | ebddres-1.2.gz | ebddres-1.2.-static.gz ]

Version 1.0 is the first public source release of EBDDRES. Version 1.1 standardized variable names but otherwise is the same as version 1.0. The gzipped tar file contains the sources, the test suite and the following README file. You may also want to have a look at our trace checker TraceCheck, which can be used to check the traces generated by EBDDRES. For version 1.2 with QDIMACS support we only provide binaries.

[ ebddres-examples.tar.gz ]

These are the examples used in the two papers on EBDDRES (see below).


In essence we use a BSD style licences for EBDDRES. Please refer to the LICENSE file for more details.


Beside being very important for testing purposes and debugging of SAT solvers, resolution proofs can be used for many other purposes, such as abstraction refinement through core generation, diagnosis of inconsistencies in product configuration and interpolation. However, it was not possible to produce resolution proofs for BDD based SAT solvers or BDD based preprocessors. The techniques implemented in EBDDRES and described in our CSR'06 paper and in our SAT'06 paper allow to add proof generation capabilities to SAT solvers that use BDD operations in one way or the other.