ABSTRACT. Expansion-based QBF solvers decide false instances by partially expanding universal variables, yielding a formula in conjunctive normal form (CNF) that can be directly refuted by a SAT solver. This approach is captured by the $\forall\text{Exp+Res}$ proof system, and certification frameworks for false QBFs have previously been presented. For true instances, the dual approach of existential expansion is less well studied. Partially expanding existential variables yields a disjunction of CNFs containing universal variables, which is not in CNF and thus cannot be passed directly to a SAT solver. Certifying true results has therefore remained an open problem. We present a proof format and checking algorithm for certifying true QBFs in the expansion-based setting, identifying and overcoming the core obstacles introduced by the necessary CNF transformation.

ABSTRACT. Almost 40 years ago, the 2-player game Connect Four was proven to be a first player win. 20 years ago, the Boolean Satisfiability community was challenged to confirm this fact by leveraging Quantified Boolean Formula techniques and associated technology. While a logic-based proof remains out of reach, several barriers have been crossed in the last few years. We report on recent progress and contrast the situation today with what it was when the challenge was first posed.

ABSTRACT. Both Quantified Boolean Formulae (QBF) as well as Dependency Quantified Boolean Formulae (DQBF) can impose spurious dependencies among variables. Since computing all spurious dependencies is in general intractable, dependency schemes are applied to detect independencies. Several dependency schemes for DQBF have been proposed in recent years. One of the strongest currently available dependency schemes is the family of implication-free dependency schemes by Beyersdorff et al. In this paper, we extend the implication-free dependency yielding an even stronger dependency scheme.

ABSTRACT. Symmetry breaking techniques have been extensively studied in automated reasoning for reducing the search space. In particular these techniques have already been well explored in the case of SAT and QBF. In this talk we discuss symmetries of dependency quantified boolean formulas (DQBF), a generalization of QBF which allows for explicit quantifier dependencies. It turns out that extending existing QBF symmetry techniques to DQBF is non-trivial due to a possible non-linear dependency structure. We illustrate these difficulties with an example that shows that a naive lifting of QBF symmetry breaking is not sufficient, and that we need more refined methods for dealing with such dependency structures.

ABSTRACT. Dependency quantified Boolean formulas (DQBF) provide a powerful, NEXPTIME-complete formalism for succinct encoding of NP-complete problems. While significant effort has been invested in developing DQBF solvers, their practical performance compared to explicit-representation solvers remains under-explored. In this work, we evaluate DQBF solving for classical succinct graph problems, such as graph coloring, $k$-clique, and Hamiltonian cycle, against traditional solvers using explicit representations. Our experimental results highlight that in general the DQBF approach is more advantageous than SAT-based approaches in handling these complex succinct combinatorial tasks.

ABSTRACT. In Quantified Boolean Formulas (QBFs), dependency schemes help identify spurious or superfluous variable dependencies introduced by the quantifier prefix but not essential for constructing countermodels. Detecting such dependencies can provably shorten refutations in certain proof systems and is expected to improve the performance of QBF solvers. Among the most prominent solving techniques for QBFs is Quantified Conflict-Driven Clause Learning (QCDCL), a generalization of CDCL to the quantified setting. The proof system defined by Beyersdorff and Boehm in \cite{BB-LMCS23} provides an abstract framework that captures the reasoning employed by QCDCL solvers. The proposed talk will describe how dependency schemes can be incorporated into QCDCL-based proof systems in various phases: during preprocessing, in the decision heuristics, or within propagation and learning.

ABSTRACT. In this work we investigate the computational complexity of the satisfiability problem of sub-fragments of the Bernays-Schoenfinkel class of first-order logic, also known as EPR (Effectively Propositional). While Bernays-Schoenfinkel is NEXPTIME-complete, we already can obtain fragments that are PSPACE-complete by restricting our clauses to DET-HORN or KROM. However such restrictions yield very different formulas to the canonical PSPACE-complete language of Quantified Boolean Formulas (QBF). This is despite Bernays-Schoenfinkel having a natural connection to an extension of QBF known as Dependency QBF. Our main contribution is the definition of a PSPACE-complete sub-fragment of Bernays-Schoenfinkel that extends from a translation of QBF, retains a similar two-player game evaluation for its semantics and can be restricted in various ways to obtain other complete problems, particularly those at different levels in the polynomial hierarchy. We use this definition to identify problems in the TPTP library that fall into this fragment and their level in the polynomial hierarchy.

ABSTRACT. In this work, we propose a knowledge compilation language for quantified Boolean formulas. We show that the language is capable of efficiently solving important QBF queries like satisfiability, model counting, MaxQBFs, and conjunctions. We also present an algorithm to compile an equivalent representation in the target language for a given QBF. Finally, we discuss some strengths and limitations of the proposed language.

ABSTRACT. Conventional notions of equivalence for quantified Boolean formulas (QBFs) consider only free variables, even though quantified variables are also relevant in many settings. Therefore, we investigated solution-based notions of equivalences that properly reflect the semantics of quantified variables. We encoded the resulting equivalence checking problem itself as a QBF and used this to implement QSOLE, the first fully automatic checker for solution-based QBF equivalence. This talk provides a summary of our work on solution-based QBF equivalences and how they can be checked.

ABSTRACT. Toda's Theorem is a fundamental result in computational complexity theory, whose proof is based on a reduction from a QBF problem with a constant number of quantifiers to a model counting problem. The recent progress in model counting tools raises the question of whether this reduction, henceforth called Toda's reduction, can be utilized to construct a practical QBF solver. This question follows a line of research that revisits theoretical results from an algorithmic aspect, thus brings new theoretical and engineering challenges. For Toda's reduction these challenges arise mainly because the reduction is purely theoretical and based on ideas that are entirely orthogonal to the search-space approach used by current QBF solvers. In this work, we address this question by transforming Toda's reduction into a concrete probabilistic QBF solver that uses model counting as an oracle. A naive implementation is hopeless due to a massive formula blow-up. Therefore we next identify three main factors that drive the blow-up. While we present solutions that overcome some of the factors, we also show that one of them, the union bound factor, largely overlooked in the literature, is in fact dominant and in some cases unavoidable. We then show how for some cases, even this factor can be avoided, and report our preliminary results on a prototype implementation.

ABSTRACT. Reactive synthesis asks for a system satisfying a given LTL specification. Bounded synthesis translates the specification to a universal co-Büchi automaton and then searches for systems of increasing size. For each size, a constraint system asserts the existence of an implementation of that size whose product with the automaton has no rejecting run. Faymonville, Finkbeiner, Rabe, and Tentrup (2017) compared SAT, QBF, and DQBF encodings of bounded synthesis and concluded that, despite being the most concise, the DQBF encodings lost to QBF because DQBF solvers were not yet competitive. Nine years on, we run a similar comparison with current state-of-the-art DQBF solvers. DQBF has narrowed the gap considerably but, in our experiments, still trails the QBF pipeline. When compared to new reactive synthesis tools, bounded synthesis has fallen behind. This gap is not entirely a solver issue: many instances are lost in the initial LTL-to-automaton translation. Encodings that bypass the automaton construction are therefore a natural target for future work.