Q-Resolution with Generalized Axioms

TL;DR

This paper introduces a generalized axiom framework for Q-resolution, significantly enhancing its power and enabling integration with other QBF solving techniques, leading to improved solver performance.

Contribution

It proposes a novel generalized axiom system for Q-resolution, allowing for stronger proofs and integration with diverse QBF solving methods.

Findings

Substantial performance improvements in QBF solving benchmarks

Effective integration of SAT solving and preprocessing techniques

Exponential increase in proof system power

Abstract

Q-resolution is a proof system for quantified Boolean formulas (QBFs) in prenex conjunctive normal form (PCNF) which underlies search-based QBF solvers with clause and cube learning (QCDCL). With the aim to derive and learn stronger clauses and cubes earlier in the search, we generalize the axioms of the Q-resolution calculus resulting in an exponentially more powerful proof system. The generalized axioms introduce an interface of Q-resolution to any other QBF proof system allowing for the direct combination of orthogonal solving techniques. We implemented a variant of the Q-resolution calculus with generalized axioms in the QBF solver DepQBF. As two case studies, we apply integrated SAT solving and resource-bounded QBF preprocessing during the search to heuristically detect potential axiom applications. Experiments with application benchmarks indicate a substantial performance improvement.