These versions are considered deprecated and are provided only for documentation. For practical applications, please always use the latest release above.
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.
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.
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.
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.
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.
For comments, questions and bug reports etc. related to DepQBF, please contact Florian Lonsing.