[  news | download | overview | publications | license ]

News

• 2012-07-18: Sources of DepQBF moved to gitHub.
• 2010-03-02: Source code of DepQBF 0.1 released.

Download

• DepQBF

Overview

DepQBF is a search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal form. It is based on the DPLL algorithm for QBF with conflict-driven clause and solution-driven cube learning. By analyzing the structure of a formula, DepQBF tries to identify independent variables. In addition to other benefits, this often increases freedom for decision making. See also the JSAT system description of DepQBF 0.1 from QBFEVAL'10 for references and a brief outline of the idea.

DepQBF 0.1 participated in QBFEVAL'10. See the competition website for performance results.

For bug reports etc., please contact Florian Lonsing.

Publications

• System description published in JSAT.
• Paper and talk at SAT'10.

License

DepQBF is released under GNU GPLv3. See also file COPYING that is part of the distribution.