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

## TL;DR

DepQBF 6.0 introduces a generalized QRES-based QCDCL solver that can produce shorter proofs for QBFs, advancing the state of the art in QBF solving techniques.

## Contribution

It presents a novel generalization of QRES within QCDCL, enabling potentially exponential proof size reductions compared to traditional methods.

## Key findings

- Generalized QRES enables shorter proofs.
- Experimental results show improved solver effectiveness.
- DepQBF 6.0 outperforms previous versions.

## Abstract

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.