EBDDRES

News

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

The latest version 1.3.1 is a maintenance release mainly to avoid warnings for more recent compilers.

Download

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.

Version 1.2 can also solve QBFs, but the exact version 1.2 used in our SAT'07 paper is unfortunately available only in binary. However, thanks to Toni Jussila, were able to resurrect some of that source code and can now also provide a slightly modified version 1.2.1.

However, you need to think of 1.2 and 1.2.1 as a seperate branch. The QBF features in 1.2 and 1.2.1 are not maintained and in particular have not been passed on to the latest version 1.3.1.

[ ebddres-examples.tar.gz ]

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

License

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

Background

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

Carsten Sinz, Armin Biere.
Extended Resolution Proofs for Conjoining BDDs.
In Proc. 1st Intl. Computer Science Symp. in Russia (CSR 2006), St. Petersburg, Russia,
Lecture Notes in Computer Science (LNCS), vol. 3967, Springer 2006.

and in our SAT'06 paper

Toni Jussila, Carsten Sinz, Armin Biere.
Extended Resolution Proofs for Symbolic SAT Solving with Quantification.
In Proc. 9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'06),
Lecture Notes in Computer Science (LNCS), vol. 4121, Springer 2006.

allow to add proof generation capabilities to SAT solvers that use BDD operations in one way or another.

In our SAT'07 paper we added support for universal quantifiers and thus QBF

Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, Christoph Wintersteiger.
A First Step Towards a Unified Proof Checker for QBF.
In Proc. 10th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'07),
Lecture Notes in Computer Science (LNCS) vol. 4501, Springer 2007.

However as described above, the corresponding features of version 1.2 used in the SAT'07 experiments have not been ported back to the main branch.