What is deescover ?

deescover is an efficient implementation of a modern conflict-driven SAT solver based on state-of-the-art techniques (1,2) such as

• conflict-driven search
• intelligent backtracking
• clause learning
• conflict-clause minimization
• restarts
• 2-watched literal scheme.

It also provides support for incremental SAT solving which is an interesting, performance improving feature for applications that create series' of related SAT problems.

Deescover is based on MiniSAT-2 which has been the winner of the international competition SAT-Race 2006 and most recently in SAT-Race 2008.

Status

• Deescover Version 0.1.1 : Minor update, May 4 2010
• Deescover Version 0.1 : Initial release, April 26, 2009

Usage

The solver can be used via a command-line interface or as a library for D applications. It can process large formulas in clause normal form.

For users that interact with the solver using the command-line interface, please use the standard text-based DIMACS CNF format to describe input formulas.

The input and output of the solver follow the specification of the SAT competition.

Performance

Our implementation is not a toy implementation. In fact, it is competitive with leading state-of-the-art systems such as Minisat 2, Picosat, or RSat. Further details for the currrent version can be found here.

Benchmark Problems

Some benchmark problems in the DIMACS CNF format:

• SATLIB Benchmark problems
• Problems used for SAT-Race 2008

References

1. M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: engineering an efficient sat solver", in DAC '01: Proceedings of the 38th conference on Design automation. New York, NY, USA: ACM Press, 2001, pp. 530-535. available online
2. N. Eén and N. Sörensson, "An extensible SAT-Solver", 2004, pp. 502-518. available online
3. N. Eén and A. Biere, "Effective Preprocessing in SAT through Variable and Clause Elimination," 2005, pp. 61-75. available online