We investigate two QBF resolution systems that use extension variables: weak extended Q-resolution, where the extension variables are quantified at the innermost level, and extended Q-resolution, where the extension variables can be placed inside the quantifier prefix. These systems have been considered previously by Wintersteiger et al, who give experimental evidence that extended Q-resolution is stronger than weak extended Q-resolution. Here we prove an exponential separation between the two systems, thereby confirming the conjecture of Wintersteiger et al. Conceptually, this separation relies on showing strategy extraction for weak extended Q-resolution by bounded-depth circuits. In contrast, we show that this strong strategy extraction result fails in extended Q-resolution.

Algorithms based on the enumeration of implicit hitting sets find a growing number of applications, which include maximum satisfiability and model based diagnosis, among others. This paper exploits enumeration of implicit hitting sets in the context of Quantified Boolean Formulas (QBF). The paper starts by developing a simple algorithm for QBF with two levels of quantification, which is shown to relate with existing work on enumeration of implicit hitting sets, but also with recent work on QBF based on abstraction refinement. The paper then extends these ideas and develops a novel QBF algorithm, which generalizes the concept of enumeration of implicit hitting sets. Experimental results, obtained on representative problem instances, show that the novel algorithm is competitive with, and often outperforms, the state of the art in QBF solving.

Many computer science problems can be naturally and compactly expressed using quantified Boolean formulas (QBFs). Evaluating thetruth or falsity of a QBF is an important task, and constructing the corresponding model or countermodel can be as important and sometimes even more useful in practice. Modern search and learning based QBF solvers rely fundamentally on resolution and can be instrumented to produce resolution proofs, from which in turn Skolem-function models and Herbrand-function countermodels can be extracted. These (counter)models are the key enabler of various applications. Not until recently the superiority of long-distanceresolution (LQ-resolution) to short-distance resolution(Q-resolution) was demonstrated. While a polynomial algorithm exists for (counter)model extraction from Q-resolution proofs, it remains open whether it exists forLQ-resolution proofs. 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 from some LQ-resolution proofs that are not obtainable from Q-resolution proofs.

A set of constraints that cannot be simultaneously satisfied is over-constrained. Minimal relaxations and minimal explanations for over-constrained problems find many practical uses. For Boolean formulas, minimal relaxations of over-constrained problems are referred to as Minimal Correction Subsets (MCSes). MCSes find many applications, including the enumeration of MUSes. Existing approaches for computing MCSes either use a Maximum Satisfiability (MaxSAT) solver or iterative calls to a Boolean Satisfiability (SAT) solver. This paper shows that existing algorithms for MCS computation can be inefficient, and so inadequate, in certain practical settings. To address this problem, this paper develops a number of novel techniques for improving the performance of existing MCS computation algorithms. More importantly, the paper proposes a novel algorithm for computing MCSes. Both the techniques and the algorithm are evaluated empirically on representative problem instances, and are shown to yield the most efficient and robust solutions for MCS computation.

When configuring customizable software, it is useful to provide interactive tool-support that ensures that the configuration does not breach given constraints. But, when is a configuration complete and how can the tool help the user to complete it? We formalize this problem and relate it to concepts from non-monotonic reasoning well researched in Artificial Intelligence. The results are interesting for both practitioners and theoreticians. Practitioners will find a technique facilitating an interactive configuration process and experiments supporting feasibility of the approach. Theoreticians will find links between well-known formal concepts and a concrete practical application.