On Expansion and Resolution in CEGAR Based QBF Solving

TL;DR

This paper compares two CEGAR-based QBF solving methods, introduces a unified calculus combining their strengths, and demonstrates experimentally that this integration improves solver performance.

Contribution

It develops a unified proof calculus that merges the strengths of existing CEGAR approaches and validates its effectiveness through implementation and experiments.

Findings

Unified calculus improves solving efficiency

Experimental results confirm theoretical advantages

Performance gains are consistent across benchmarks

Abstract

A quantified Boolean formula (QBF) is a propositional formula extended with universal and existential quantification over propositions. There are two methodologies in CEGAR based QBF solving techniques, one that is based on a refinement loop that builds partial expansions and a more recent one that is based on the communication of satisfied clauses. Despite their algorithmic similarity, their performance characteristics in experimental evaluations are very different and in many cases orthogonal. We compare those CEGAR approaches using proof theory developed around QBF solving and present a unified calculus that combines the strength of both approaches. Lastly, we implement the new calculus and confirm experimentally that the theoretical improvements lead to improved performance.