A solver for quantified boolean formulae (QBF)
PLEASE NOTE: The installation process has changed. Run the script 'compile.sh' instead of 'make'. See also the README file that is part of the distribution.
DepQBF is released under GNU GPLv3. Source code is available from GitHub at https://github.com/lonsing/depqbf. Alternatively, source code can be downloaded here.
These versions are considered deprecated and are provided only for documentation. For practical applications, please always use the latest release above (unless stated otherwise).
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, called QDPLL, with conflict-driven clause and solution-driven cube learning.
By analyzing the syntactic structure of a formula, DepQBF tries to identify independent variables. In general, information on independent variables can be represented in the formal framework of dependency schemes. DepQBF computes the so-called "standard dependency scheme" of a given formula. In addition to other benefits, information on independent variables often increases the freedom for decision making and clause learning. See also the JSAT system description of DepQBF for references and a brief outline of the idea.
In addition to the use of advanced dependency schemes, DepQBF also supports solving with respect to the linear ordering of the quantifier prefix in the given formula.
Since version 3.0, DepQBF comes with an API which allows for incremental solving based on a clause stack. Clauses can be added to and removed from the current formula by push and pop operations. Incremental solving can be beneficial in applications where a sequence of closely related formulae must be solved. This way, the solver does not have to solve each formula from scratch but tries to reuse information learned from previously solved formulae.
Version 4.0 (or later) provides an API for incremental solving by clause groups. A clause group is a set of clauses which is incrementally added to and deleted from the formula. The clause group API generalizes the push/pop API and is suitable for incremental applications where the underlying formula is modified in a non-uniform way. The design of the clause group API is inspired by the SAT solver zChaff. Implementation details and an overview of the API can be found in the following tool paper:
Florian Lonsing and Uwe Egly: Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. 6-page tool paper, proceedings of SAT 2015, LNCS, Springer. Preprint of proceedings version with appendix (PDF).
The clause group API of DepQBF version 4.0 (or later) allows for a convenient extraction of unsatisfiable cores of QBFs.
Please see the README file for important guidelines on incremental solving and API usage.
Since version 3.0, assumptions can be added through the API of DepQBF. Assumptions are fixed variable assignments from the leftmost quantifier block of a QBF. In forthcoming calls, the solver tries to solve the formula under the assignments given by the added assumptions. Solving under assumptions is commonly used in workflows based on incremental SAT solving. In DepQBF, assumptions can be used as an alternative to the push and pop operations to support incremental QBF solving.
For performance reasons, however, it is recommended to use either the push/pop API or the clause group API for incremental solving.
The latest release comes with examples which illustrate the use of the API of DepQBF for incremental solving and solving under assumptions. Please see the README file of the latest release for further information.
The slides presented at the ReRiSE'14 Winter School give an overview of the API of DepQBF: slides.
DepQBF4J enables Java applications to use DepQBF as a library. It provides a wrapper for the API functions of DepQBF which is implemented using the Java Native Interface (JNI). Using DepQBF as a library within other programs avoids I/O overhead and allows for a tighter integration of DepQBF in QBF-based workflows.
The purpose of DepQBF4J is to make QBF solving more accessible to users who prefer Java over C and who are interested in using QBF as a modeling language for their applications.
The latest release of DepQBF (version 3.03 or later) includes DepQBF4J in a subdirectory, including Java code examples. You can browse the code of DepQBF4J here.
Traditional Q-resolution as introduced in H. Kleine Büning, M.Karpinski, A. Flögel: Resolution for Quantified Boolean Formulas. Inf. Comput. 117(1): 12-18 (1995) explicitly rules out the generation of tautological resolvents. In contrast to that, long-distance resolution admits certain tautological resolvents. It was first implemented in the QBF solver quaffle and is now also available in DepQBF.
Version 5.0 of DepQBF (or any later version) includes blocked clause elimination (QBCE) as a pre- and inprocessing technique and as a novel dynamic approach (enabled by default) where QBCE is interleaved with the search process. The QBCE variants are currently available only in non-incremental mode.
It is recommended to run DepQBF in its default configuration, which has dynamic QBCE enabled. Alternatively, QBCE pre- and inprocessing may be enabled via command line arguments. Depending on your application, preprocessors such as Bloqqer or QxBF, for example, may improve the performance of DepQBF further.
HOWEVER: depending on the given instance, preprocessing by Bloqqer may be harmful to the performance of DepQBF version 5.0 in its default configuration (using dynamic QBCE).
Since version 1.0, DepQBF is able to produce clause/term resolution proofs of (un)satisfiability for a given formula. Given a resolution proof, it is possible to obtain a set of Skolem/Herbrand functions by an approach introduced in the paper V. Balabanov and J. R. Jiang: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications. CAV 2011. This set of functions is a certificate of (un)satisfiability of the formula.
The framework QBFcert provides a set of tools for resolution proof extraction and checking, certificate extraction and certificate validation.
Lists of instances from QBFEVAL'08 and QBFEVAL'10 which have been certified using DepQBF and QBFcert are available from the QBFcert webpage.
For comments, questions and bug reports etc. related to DepQBF, please contact Florian Lonsing.