DepQBF

A solver for quantified boolean formulae (QBF)

News

Source Code

DepQBF is released under GNU GPLv3. Source code is available from GitHub at https://github.com/lonsing/depqbf. Alternatively, source code can be downloaded using the links below.

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.

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.

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.

Preprocessing

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.

Contact

For comments, questions and bug reports etc. related to DepQBF, please contact Florian Lonsing.

Publications