This directory contains the source code of the SAT solver EBDDRES. To compile it run './configure; make'. Then you should run the test suite with './test'. If you do not have the trace checker 'tracecheck' binary in your path then the generated traces can are not checked. The source code is available under the conditions described in the file 'LICENSE'. More information on EBDDRES can be found in the following two publications C. Sinz, A. 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 T. Jussila, C. Sinz, A. Biere. Extended Resolution Proofs for Symbolic SAT Solving with Quantification. In Proc. 9th Intl. Conf. on Theory and Applications of Satisfiability Testing Seattle (SAT 2006), August, 2006, vol. 4121, Springer 2006. Armin Biere, Linz, June 2006.