Bridging the gap between dual propagation and CNF-based QBF solving

Conjunctive Normal Form (CNF) representation as used by most modern Quantified Boolean Formula (QBF) solvers is simple and powerful when reasoning about conflicts, but is not efficient at dealing with solutions. To overcome this inefficiency a number of specialized non-CNF solvers were created. These solvers were shown to have great advantages. Unfortunately, non-CNF solvers cannot benefit from sophisticated CNF-based techniques developed over the years. This paper demonstrates how the power of non-CNF structure can be harvested without the need for specialized solvers; in fact, it is easily incorporated into most existing CNF-based QBF solvers using a pre-existing mechanism of cube learning. We demonstrate this using a state-of-the-art QBF solver DepQBF, and experimentally show the effectiveness of our approach.