# DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL

arXiv: https://arxiv.org/abs/1702.08256 · HTML: https://mlsanity.com/paper/1702.08256/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Feb 2017.

## Built on by (most cited first, 8 of 8)

- [Planning with Incomplete Information in Quantified Answer Set Programming](https://mlsanity.com/paper/2108.06405/) (2021)
- [DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving](https://mlsanity.com/paper/2205.03747/) (2022)
- [Implicit State and Goals in QBF Encodings for Positional Games (extended version)](https://mlsanity.com/paper/2301.07345/) (2023)
- [Program Synthesis as Dependency Quantified Formula Modulo Theory](https://mlsanity.com/paper/2105.09221/) (2021)
- [Synthesis with Explicit Dependencies](https://mlsanity.com/paper/2301.10556/) (2023)
- [Concise QBF Encodings for Games on a Grid (extended version)](https://mlsanity.com/paper/2303.16949/) (2023)
- [Tackling Universal Properties of Minimal Trap Spaces of Boolean Networks](https://mlsanity.com/paper/2305.02442/) (2023)
- [An Expansion-Based Approach for Quantified Integer Programming](https://mlsanity.com/paper/2506.04452/) (2025)

## Abstract (arXiv)

We present the latest major release version 6.0 of the quantified Boolean formula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension of the conflict-driven clause learning (CDCL) paradigm implemented in state of the art propositional satisfiability (SAT) solvers. The Q-resolution calculus (QRES) is a QBF proof system which underlies QCDCL. QCDCL solvers can produce QRES proofs of QBFs in prenex conjunctive normal form (PCNF) as a byproduct of the solving process. In contrast to traditional QCDCL based on QRES, DepQBF 6.0 implements a variant of QCDCL which is based on a generalization of QRES. This generalization is due to a set of additional axioms and leaves the original Q-resolution rules unchanged. The generalization of QRES enables QCDCL to potentially produce exponentially shorter proofs than the traditional variant. We present an overview of the features implemented in DepQBF and report on experimental results which demonstrate the effectiveness of generalized QRES in QCDCL.