Quantified Boolean Formulas (QBFs) extend propositional logic with existential and universal quantifiers, making their decision problem PSPACE-hard. Recent advances in QBF solvers have established QBFs as an attractive framework for encoding PSPACE-hard problems across domains such as formal verification, synthesis, and symbolic AI. Despite progress in solving techniques, less attention has been given to the infrastructure for constructing correct and efficient QBF encodings. For instance, it is often unclear whether two QBFs that encode the same problem in different ways yield the same solutions. Traditional QBF equivalence checking focuses only on free variables, yet in many cases, the quantified variables must also be considered. In this paper, we present QSOLE , the first fully automatic checker for solution-based QBF equivalence. Based on a recently introduced approach, QSOLE decomposes equivalence checks into smaller entailment computations and is capable of generating witnesses for detected inequivalences, which can be used to debug encodings. Furthermore, it allows for explicit exclusion of variables from equivalence checks enabling comparison of formulas using different local auxiliary variables.

Over the last years many solvers for quantified Boolean formulas (QBFs) have been developed. While most of these solvers support QDIMACS as a standard input format, exchanging a QBF solver within a reasoning framework is often a challenging task. Many solvers do not provide an API but they can only be used via their executable. Further, incremental solving is only supported to a limited extent. We present PyQBF , a Python-based framework that provides a uniform programmatic interface to state-of-the-art QBF solvers. In this article, we introduce the general architecture of PyQBF , describe the supported features and give a detailed example that illustrates how our framework can be used to implement an enumerative QBF solution counter as well as to solve a bounded model checking problem using a non-CNF representation. Our extensive experimental evaluation shows the efficiency of PyQBF . The experiments indicate that there is only little overhead compared with direct usage of the solvers.