ABSTRACT. For quantified Boolean formulas (QBFs), preprocessing is essential to solve many real-world formulas. The application of a preprocessor, however, prevented the extraction of proofs for the original formula. Such proofs are required to independently validate correctness of the preprocessor's rewritings and the solver's result. Especially for universal expansion proof checking was not possible so far. In this talk, we present a unified proof system based on three simple and elegant quantified resolution asymmetric tautology QRAT rules. In combination with an extended version of universal reduction, they are sufficient to efficiently express all preprocessing techniques used in state-of-the-art preprocessors including universal expansion. Moreover, these rules give rise to new preprocessing techniques. We equip the preprocessor bloqqer with QRAT proof logging and provide a proof checker for QRAT proofs.

ABSTRACT. Several calculi for quantified Boolean formulas (QBFs) exist but relations between them are not yet fully understood. This talk defines a novel calculus, which is resolution-based and enables unification of Q-resolution and the expansion-based calculus ∀Exp+Res. These calculi play an important role in QBF solving. This talks shows simulation results for the new calculus and discusses further possible extensions of the calculus.

ABSTRACT. Quantified Boolean formulas (QBFs) generalize propositional formulas by admitting quantifications over propositional variables. QBFs can be viewed as (restricted) formulas of first-order predicate logic and easy translations from QBFs to first-order formulas exist. We analyze the effect of such a translation on the complexity of resolution proofs. More precisely, we show that there are classes $(\Phi_i)_{i\geq 1}$ of QBFs where any Q-resolution refutation of $\Phi_i$ has length super-polynomial in $i$, but the translated version of $\Phi_i$ possesses a short resolution refutation. Moreover we discuss that first-order predicate logic can be used to succinctly represent refutations of QBFs obtained in different QBF calculi.

ABSTRACT. We define Q(D)-term resolution, a family of proof systems for true Quantified Boolean Formulas (QBFs). These systems are generalizations of term resolution that capture the proof system(s) used by DepQBF to generate proofs of true formulas. DepQBF implements a version of the QCDCL algorithm that is parameterized by a so-called dependency scheme, a mapping that associates each formula with a binary relation on its variables that represents potential variable dependencies. Similarly, Q(D)-term resolution is parameterized by a dependency scheme D. We show that Q(Dres)-term resolution is sound, where Dres is the so-called Resolution-path Dependency Scheme. This entails soundness of Q(Dst)-term resolution, where Dst is the Standard Dependency Scheme currently implemented in DepQBF.

ABSTRACT. Resolution is a fundamental part of modern search and learning based QBF solvers, and the extraction of Skolem-function models and Herbrand-function countermodels from QBF resolution proofs is a key enabler for various applications. Although long-distance resolution (LQ-resolution) came into existence a decade ago, its superiority to short-distance resolution (Q-resolution) was not recognized until recently. It remains open whether there exists a polynomial time algorithm for model and countermodel extraction from LQ-resolution proofs, although an efficient algorithm does exist for the Q-resolution counterparts. This paper settles this open problem affirmatively by constructing a linear-time extraction procedure. Experimental results show the distinct benefits of the proposed method in extracting high quality certificates.

ABSTRACT. We will give an introduction into Dependency Quantified Boolean Formulas (DQBF)
which generalize Quantified Boolean Formulas (QBF).
After briefly reviewing the complexity of the problem we will
present the partial equivalence checking problem (PEC) which requires
general DQBF formulations for exact solutions.
To solve PEC (which checks whether a given partial implementation of a combinational circuit can still
be extended to a complete design that is equivalent to a given full specification)
we give a linear transformation from PEC to the question whether a
Dependency Quantified Boolean Formula (DQBF) is satisfied.
We present first algorithmic solutions to the satisfiability of DQBF.
Preliminary experimental results show the feasibility of our approach
as well as the inaccuracy of QBF approximations, which were used for deciding PEC so far.

ABSTRACT. Incremental solving methods made SAT attractive for industrial use as core technology of numerous electronic design automation tools, e.g. for verification tasks like Bounded Model Checking (BMC). On the other hand, when dealing with partial designs or unknown specifications, SAT formulas are not expressive enough, whereas a description via quantified Boolean formulas (QBF) is more adequate. 

Persuaded by the success of incremental SAT, we explore various ways to tackle QBF problems incrementally and thereby make this technology available. We developed the first incremental QBF solver based on the state-of-the-art QBF solver QuBE, which can now reuse some information from previous iterations, therefore pruning the search space. 

However, the need for a preprocessing QBF phase, that in general cannot be paired with incremental solving because of the non-predictable elimination of variables in the future incremental steps, posed the question of incremental QBF preprocessing. We study an approach for retaining the QBF formula being preprocessed while extending its clauses and prefix incrementally. This procedure yields effectively preprocessed QBF formulas, nevertheless it may come together with long runtimes. We consider various heuristics to dynamically skip incremental preprocessing when its overhead is not compensated by the reduced solving time anymore.

We experimentally analyze from both the point of view of the effectiveness of the single procedure and how a generic QBF solver can profit from it how the different methods positively affect BMC for partial designs (i.e. designs containing so-called blackboxes which represent unknown parts). The goal of this problem is to disprove realizability, that is, to prove that an unsafe state is reachable no matter how the blackboxes are implemented. On a domain of partial design benchmarks, engaging incremental QBF methods significant performance gains over non incremental BMC can be achieved.   

ABSTRACT. Reactive synthesis algorithms construct a correct reactive system fully automatically from a given formal specification. Besides the construction of full systems, such synthesis algorithms are also used for program sketching and automatic program repair. This talk will explain how reactive synthesis can be realized efficiently with QBF solving, and how recently proposed approaches for incremental QBF solving can be exploited. We present first experimental results and compare our QBF-based solution to SAT- and BDD-based implementations.

ABSTRACT. We consider planning with uncertainty in the initial state as a case study of incremental quantified Boolean formula (QBF) solving. We report on experiments with a workflow to incrementally encode a planning instance into a sequence of QBFs. To solve this sequence of incrementally constructed QBFs, we use our general-purpose incremental QBF solver DepQBF. Since the generated QBFs have many clauses and variables in common, our approach avoids redundancy both in the encoding phase and in the solving phase. Experimental results show that incremental QBF solving outperforms non-incremental QBF solving. Our results are the first empirical study of incremental QBF solving in the context of planning. Based on our case study, we argue that incremental QBF solving also has the potential to improve QBF-based workflows in other application domains.

ABSTRACT. We revisit the interactive consistency problem introduced
by Pease, Shostak and Lamport.  We first show that their
algorithm does not achieve interactive consistency if
faults are transient, even if faults are non-malicious. 
We then present an algorithm that achieves interactive
consistency in the presence of non-malicious, asymmetric
and transient faults, but only under an additional
guaranteed delayed ack assumption.

We discovered our algorithm
using an automated synthesis technique that is based on
bounded model checking and QBF solving.  Our synthesis
technique is general and simple, and it is a promising
approach for synthesizing distributed algorithms.
We also illustrate the use of our synthesis approach on
a self-stabilizing mutual exclusion algorithm introduced by Dijkstra.