DepQBF

News

• 2018-05-03: In a related project, we developed the novel QBF preprocessor QRATPre+ based on the QRAT+ proof system. A paper presenting QRAT+ will be published at IJCAR 2018.
• 2017-08-02: Source code of DepQBF 6.03 released (minor maintenance release).
• 2017-06-08: New system description of DepQBF accepted at CADE 2017: DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. This new system description describes version 6.0 (or later) of DepQBF and supersedes the old system description published in JSAT, 2010. A preprint of the proceedings version with appendix is available (PDF).
• 2017-03-27: Source code of DepQBF 6.02 released. In this release Bloqqer is replaced by the QBF solver Nenofex. This replacement was necessary since Bloqqer is not reentrant, which may cause problems when creating multiple instances of DepQBF.
• 2017-02-28: Source code of DepQBF 6.01 released. This release fixes a memory error and allows for the compilation without using the preprocessor Bloqqer as a library. To compile without Bloqqer, run './compile.sh nobloqqer' in the DepQBF directory.
• 2017-02-20: Source code of DepQBF 6.0 released. This release implements conflict-driven clause and solution-driven cube learning (QCDCL) with generalized axioms. To this end, DepQBF applies the SAT solver PicoSAT and the QBF preprocessor Bloqqer as oracles to check the satisfiability of formulas that arise in the context of axiom applications. The approach is described in our SAT 2016 paper.

  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.

• 2016-09-09: Source code of DepQBF 5.01 released. This release fixes a bug in the generation of QDIMACS output.
• 2016-08-12: DepQBF achieved a 3rd place in the Prenex CNF track and a 3rd place in the 2QBF track of the QBFEVAL'16 competition.
• 2015-12-15: QBF Workshop 2016 affiliated to SAT 2016.
• 2015-10-26: Source code of DepQBF 5.0 released. This release includes blocked clause elimination (QBCE) both as a pre- and inprocessing technique and as a novel dynamic variant for cube learning. The approach is described in our LPAR 2015 paper. See also the notes on preprocessing below.
• 2015-06-09: Source code of DepQBF 4.01 released.
• 2015-02-19: Source code of DepQBF 4.0 released, including a novel API for incremental solving.
• 2015-02-19: QBF Workshop 2015 affiliated to SAT 2015.
• 2015-01-26: QUANTIFY Workshop 2015 affiliated to CADE 2015.
• 2014-09-30: Source code of DepQBF 3.04 released.
• 2014-07-17: DepQBF wins four medals:
  • Kurt Gödel Society silver medal at the FLoC Olympic Games 2014.
  • Silver medal in the CNF Track of the QBF Gallery 2014.
  • Silver medal in the Preprocessing Track of the QBF Gallery 2014.
  • Bronze medal in the Applications Track of the QBF Gallery 2014.
• 2014-05-09: Source code of DepQBF 3.03 released, including DepQBF4J.
• 2014-04-23: Source code of DepQBF 3.02 released.
• 2014-04-15: Source code of DepQBF 3.01 released.
• 2014-02-12: Source code of DepQBF 3.0 released.
• 2014-02-12: DepQBF at the ReRiSE'14 Winter School.
• 2014-02-12: QBF Gallery 2014 affiliated to SAT 2014.
• 2014-02-12: QBF Workshop 2014 affiliated to SAT 2014.
• 2014-02-12: QUANTIFY Workshop 2014 affiliated to IJCAR 2014.
• 2013-08-28: Source code of DepQBF 2.0 released.
• 2013-01-18: QBF Gallery 2013 affiliated to SAT 2013.
• 2013-01-17: QBF Workshop 2013 affiliated to SAT 2013.
• 2012-09-05: Added information on certificates.
• 2012-07-18: Source code of DepQBF 1.0 released.
• 2010-03-02: Source code of DepQBF 0.1 released.

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 here.

Latest release

• Version 6.03 (source code), see the README file for release notes.

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).

• Version 6.02 (source code).
• Version 6.01 (source code).
• Version 6.0 (source code).
• Version 5.01 (source code).
• Version 5.0 (source code).
• Version 4.01 (source code).
• Version 4.0 (source code).
• Version 3.04 (source code).
• Version 3.03 (source code).
• Version 3.02 (source code).
• Version 3.01 (source code).
• Version 3.0 (source code).
• Version 2.0 (source code).
• Version 1.0 (source code).

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, proceedings of SAT 2015, LNCS, Springer. 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.

• Example: basic use, push/pop API
• Example: clause group API

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

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).

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

• New system description to appear at CADE 2017: F. Lonsing and U. Egly: DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL. In Proc. 26th International Conference on Automated Deduction (CADE-26), LNCS, Springer, 2017, to appear. Preprint of proceedings version with appendix (PDF).
• Paper at SAT 2016 on QCDCL with generalized axioms: F. Lonsing, U. Egly, and M. Seidl: Q-Resolution with Generalized Axioms. In Proc. 19th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2016), LNCS, Springer, 2016. Preprint of proceedings version with appendix (PDF).
• Paper at LPAR 2015 on dynamic blocked clause elimination (QBCE): F. Lonsing, F. Bacchus, A. Biere, U. Egly, and M. Seidl: Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. In Proc. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2015), LNCS, Springer, 2015. To appear. Preprint of proceedings version (PDF).
• Tool paper at SAT 2015 on clause groups and minimal unsatisfiable cores: Florian Lonsing and Uwe Egly: Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. Proc. SAT 2015. Preprint of proceedings version with appendix (PDF).
• Paper at AISC 2014 on conformant planning as an application of incremental solving: U. Egly, M. Kronegger, F. Lonsing, and A. Pfandler: Conformant Planning as a Case Study of Incremental QBF Solving. Proc. 12th International Conference on Artificial Intelligence and Symbolic Computation (AISC), volume 8884 of Lecture Notes in Artificial Intelligence (LNAI), Springer, 2014. Preprint.
• Paper at CP 2014 on incremental QBF solving: Florian Lonsing and Uwe Egly. Incremental QBF Solving. In Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming, LNCS, Springer, 2014. (Preprint).
• Extended abstract at ICMS 2014 on incremental QBF solving: Florian Lonsing and Uwe Egly. Incremental QBF Solving by DepQBF. In Proceedings of the 4th International Congress on Mathematical Software (ICMS 2014), LNCS, Springer 2014.
• Paper at LPAR'13 on long-distance resolution implemented in DepQBF 3.0: U. Egly, F. Lonsing, and M. Widl. Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving. In Proc. LPAR 2013.
• Paper at SAT'13 on QPUP-based clause and cube learning implemented in DepQBF 2.0: F. Lonsing, U. Egly, and A. Van Gelder. Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. SAT 2013.
• System description published in JSAT: PDF
• Slides of related talk at Pragmatics of SAT 2010 workshop: PDF.
• Tool paper at SAT'12 on QBF certification: A. Niemetz, M. Preiner, F. Lonsing, M. Seidl and A. Biere: Resolution-Based Certificate Extraction for QBF (Tool Presentation). SAT 2012.
• Dissertation by Florian Lonsing.