Refinement-Based Enumeration of QBF Solutions

Counting the number of solutions of true and false quantified Boolean formulas (QBFs) has received increased interest in recent years. However, the explicit enumeration of all solutions for a QBF is almost unexplored so far. For QBF solution counting, it has been shown that enumeration-based counting as employed in SAT is not complete for QBF. Solution enumeration runs into the same problem. We propose a refinement-based approach to enumerate (all) solutions of true and false QBFs. To this end, we develop a novel framework to characterize the enumeration problem at quantifier level two and present a complete enumeration algorithm that can be interrupted at any time as soon as enough solutions are found. We evaluated our implementation called QEnum in three different case studies.