A solver for quantified boolean formulae (QBF)


Source Code

DepQBF is released under GNU GPLv3. Source code is available from GitHub at Alternatively, source code can be downloaded here.

Latest release

Previous versions

These versions are considered deprecated and are provided only for documentation. For practical applications, please always use the latest release above (unless stated otherwise).

General Information

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.

Incremental Solving

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, to appear in proceedings of SAT 2015. Preprint of proceedings version with appendix (PDF).

Unsatisfiable Cores

The clause group API of DepQBF version 4.0 (or later) allows for a convenient extraction of unsatisfiable cores of QBFs.

Notes on API Usage

Please see the README file for important guidelines on incremental solving and API usage.

Solving under Assumptions

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.

API Examples

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: A Java Interface of DepQBF

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.

Long-Distance Resolution

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.


DepQBF does NOT include preprocessing, apart from cleaning up the input formula by removing tautological clauses and duplicate literals from clauses.

Preprocessing is usually important for the performance of QBF-based workflows. For QBF preprocessing tools, we refer to Bloqqer or QxBF, for example.

Proofs and Certificates

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.