ABSTRACT. Treewidth is a well-studied decompositional parameter to measure the tree-likeness of a graph. While the propositional satisfiability problem (SAT) is known to be tractable when parameterized by the treewidth of the underlying primal graph, the evaluation of quantified Boolean formulas (QBFs) remains PSPACE-complete even on formulas of constant treewidth. Intuitively, this is because ordinary treewidth does not take into account the prefix of the QBF: it neither distinguishes between existential and universal variables, nor accounts for the order in which they are quantified. In the past, several weaker variants of treewidth have been devised to incorporate prefix-sensitive information. To establish tractability for QBFs under these notions, prior work has employed either strategy- or resolution-based techniques, thereby dividing the parameterized complexity landscape of QBF into two regimes that are incomparable in strength. We establish fixed-parameter tractability with respect to bilateral treewidth, a novel and strictly more powerful decompositional parameter that combines these rivaling approaches by simultaneously allowing for branching on strategies and performing Q-resolution.

ABSTRACT. CAQE (Clausal Abstraction for Quantifier Elimination) is currently the most successful algorithmic paradigm for solving Quantified Boolean Formulas (QBF) practice-wise, clearly dominating recent QBF competitions. While apparently being a very strong solver, not much is known about CAQE theory-wise. We propose a framework for formalising CAQE runs which we use to analyse the algorithm proof-theoretically. We show that one can perform strategy extraction on that CAQE proof system in such a way that strategy size serves as a lower bound for CAQE runs. Furthermore, we introduce a measure, which we call CAQE width, which not only acts as a lower bound on CAQE proofs, but — with the quantifier depth as exponent — as an upper bound as well. Using this analysis, we prove that on QBFs of bounded quantifier complexity, both QCDCL (Quantified Conflict Driven Clause Learning, formalised as a proof system) and Q-resolution p-simulate CAQE and are indeed strictly stronger. Hence, as proof systems, QCDCL is provably better than CAQE, contrary to their relative performance in practice.

ABSTRACT. Quantified Boolean Formula (QBF) is a notoriously hard generalization of \textsc{SAT}, especially from the point of view of parameterized complexity, where the problem remains intractable for most standard parameters. A recent work by Eriksson et al.~[IJCAI 24] addressed this by considering the case where the propositional part of the formula is in CNF and we parameterize by the number $k$ of existentially quantified variables. One of their main results was that this natural (but so far overlooked) parameter does lead to fixed-parameter tractability, if we also bound the maximum arity $d$ of the clauses of the given CNF. Unfortunately, their algorithm has a \emph{double-exponential} dependence on $k$ ($2^{2^k}$), even when $d$ is an absolute constant. Since the work of Eriksson et al.\ only complemented this with a SETH-based lower bound implying that a $2^{O(k)}$ dependence is impossible, this left a large gap as an open question. Our main result in this paper is to close this gap by showing that the double-exponential dependence is optimal, assuming the ETH: even for CNFs of arity $4$, QBF with $k$ existential variables cannot be solved in time $2^{2^{o(k)}}|\phi|^{O(1)}$. Complementing this, we also consider the further restricted case of QBF with only two quantifier blocks ($\forall\exists$-QBF). We show that in this case the situation improves dramatically: for each $d\ge 3$ we show an algorithm with running time $k^{O_d(k ^{d-1})}|\phi|^{O(1)}$ and a lower bound under the ETH showing our algorithm is almost optimal.

ABSTRACT. A variable in a quantified Boolean formula (QBFs) is defined, if its value is uniquely determined by some other variables. Such definitions are widely exploited in various techniques for QBF solving. In this work, we formalize the concept of using definitions for reducing variable dependencies by introducing a novel dependency scheme and investigate its proof-theoretic impact. Our analysis shows that a definition-based dependency scheme is able to detect independencies other established dependency schemes cannot and that this can lead to exponentially shorter refutations. We further demonstrate that our scheme can be combined with any other scheme and that such a combined use can exponentially outperform using either scheme alone. Moreover, we study the dynamic application of our definition-based dependency scheme, which leads to another exponential speedup compared to the static application. Finally, we analyze the computational complexity of our dependency scheme and introduce a family of efficiently computable variants.

ABSTRACT. Certification for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF) is an ongoing challenge. Recent proof complexity work has shown that the majority of QBF and DQBF techniques can be p-simulated by using the independent extension rule. In propositional logic, extension rules are supported by proof checkers using a more general RAT (Resolution Asymmetric Tautology) rule. The obvious next step in (D)QBF certification would be to update these modern RAT formats to match the strength of this independent extension rule. In this paper we first introduce a new dependency scheme called Dpure, this rule is the missing ingredient that when added to Blinkhorn's proof system DQRAT allows it to be p-equivalent to the Independent Extended QU-Res, the most powerful of the known QBF and DQBF proof systems. Up until now, DQRAT has only existed in theory, so we implement a prototype checker DQRAT-check which includes our extra rule. In addition to its inclusion in our proof checker we show Dpure has two other properties that have been found for previous dependency schemes, and each of these observations has potential in solving/checking. We demonstrate a strategy extraction theorem for long distance Q-resolution equipped with Dpure, meaning it can be incorporated soundly into the dependency learning solver Qute.

ABSTRACT. Strategy extraction in QBF proof systems usually attempts to extract winning strategies from valid proofs. However, an alternative (and arguably more powerful) view is to extract Skolem/Herbrand functions, or equivalently synthesis of the game values at all intermediate points. In this paper, we investigate the existence and properties of such proof systems from which one can extract Skolem and Herbrand functions. We propose such a proof system for QBF, which we show is sound and complete, and from which extraction of Skolem/Herbrand functions can be performed, and game values computed, in polynomial time. We also show that this system is optimal among all proof systems that allow efficient extraction of Skolem/Herbrand functions. We provide conditional lower bound results for our new proof system and compare it to several existing/standard proof systems for QBF that have been studied in the literature, showing interesting orthogonality results. Finally, we provide a compilation algorithm that takes an arbitrary QBF and synthesizes a proof in our system, from which Skolem and Herbrand functions can be easily computed.

ABSTRACT. For a quantified Boolean formula (QBF), the problem of computing the number of winning strategies is known as the #QBF problem. This problem is considered harder than the analogous #SAT problem. Recently, important proof systems for QBFs and #SAT have been studied. By extending the ideas from both fields, we show that it is possible to design proof systems for #QBF. Such proof systems are important not only for advancing the theory of #QBF but also for certifying and designing better #QBF solvers, an area that is still in its early stages. In this paper, we explore #QBF proof systems to count the number of Skolem functions. Apart from a naive system, we study #QBF systems based on the expansion rule of universal variables in QBFs. We observe that these systems have inherent structural weaknesses that lead to lower bounds. As an alternative, we propose a #QBF proof system that we call Q-MICE, which consists of sound inference rules for computing and certifying the #QBF solution, similar to the line-based #SAT proof system MICE. To demonstrate the strength of Q-MICE, we present various upper bounds, such as the quantified version of the propositional XOR-PAIRS formula, which are known to be hard for MICE. Consequently, we also separate Q-MICE from the expansion-based #QBF proof systems.

ABSTRACT. We describe a procedure that extracts existential strategies from verification proofs in the Long-Distance Consensus (i.e.\ Term-Resolution) proof system when augmented with dependency schemes. We prove that when the standard dependency scheme D^{std} is used, the extracted strategies are winning strategies, thus establishing soundness of the proof system LDQ(D^{std})Consensus. We show through a counterexample that this approach fails to show soundness for LDQ(D^{rrs})Consensus.

ABSTRACT. Knowledge compilation transforms logical theories into circuit representations that support efficient reasoning. We study this problem for propositional groundings of FO2, the two-variable fragment of first-order logic over finite domains. Given an FO2 sentence and a domain of size n, its grounding yields a propositional theory over ground atoms. We ask whether such theories admit compact DNNF-based representations and whether these can be constructed efficiently, both with respect to the domain size n for a fixed sentence. We show first that compact compilation is impossible in general: there exists a FO2 sentence whose grounding over a domain of size n requires DNNF size $2^{\Omega(n)}$. On the positive side, we develop a two-stage d-DNNF compiler that exploits the symmetries inherent in the propositional groundings of FO2 sentences. It branches on unary and binary types rather than individual ground atoms, in a similar spirit to lifted inferences for probabilistic relational models. Moreover, it optimizes the compilation process by caching and reusing compiled subcircuits by identifying residual subproblems that are equivalent with respect to future extensions. Experiments on several benchmark families show that our approach generally yields substantially smaller circuits than straightforward grounding-and-then-compiling baselines.

ABSTRACT. The well-founded semantics (WFS) for logic programs results in a unique three-valued interpretation and serves as an efficient basis for skeptical reasoning, but lacks built-in mechanisms for objective choice and case-based reasoning, limiting its expressiveness for decision problems. Propositional SAT solvers excel at the latter but, unlike WFS, do not naturally admit reasoning under uncertainty or encoding transitive closure properties. We present an integration of an objective choice operator into WFS that preserves the semantics' suitability for scalable, partial-information reasoning and show that this choice operator can be materialized by a SAT solver while propagating the consequences of choices through an extension of the well-established alternating fixed-point algorithm for WFS with conflicts being propagated back to the SAT solver. We illustrate the approach in a setting for reasoning about actions under uncertainty, and we extend the framework to support theory constraints, such as difference logic constraints for modeling actions with duration. From a propositional perspective, our semantics gracefully captures semantically unassigned atoms and constraints. We study syntactic decomposition techniques for logic programs with choices, benefiting both grounding and solving. Finally, we relate our semantics to answer sets, and demonstrate that classical propositional satisfiability can not only be embedded in our framework, but can now also be extended with reasoning over transitive closures.

ABSTRACT. Discrete variables are common in many applications, such as probabilistic reasoning, planning and explainable AI. When symbolic reasoning techniques are brought in to bear on these applications, a standard technique for handling discrete variables is to binarize them into Boolean variables to allow the use of Boolean computational machinery such as SAT solvers. This technique can face both computational and semantical challenges though. In this work, we develop a native SAT solver for discrete logic, which is a direct extension of Boolean logic in which variables can take arbitrary values. Our proposed solver has a similar design to Boolean SAT solvers, with ingredients such as unit resolution and clause learning but ones that operate natively on discrete variables. We illustrate the merits of the developed SAT solver by comparing it empirically to CSP solvers applied to discrete CNFs, to Boolean SAT solver applied to binarized CNFs, and to some hybrid solvers.

ABSTRACT. Because CDCL produces proofs in the Resolution proof system, problems provably hard for Resolution are also provably hard for CDCL. Exponentially shorter proofs can sometimes be found using stronger proof systems such as $\text{Res}(\oplus)$, a generalization of Resolution to XNF formulas, whose constraints are disjunctions of parity equations (``linear clauses'') such as $(x \oplus y) \lor \lnot (y \oplus z)$. While some modern solvers like CryptoMiniSAT reason on Boolean clauses with separate parity equations, reasoning about more general linear clauses is less explored. We present $\text{CDCL}(\oplus)$, a generalization of CDCL to XNF formulas, and prove a bidirectional connection with $\text{Res}(\oplus)$: $\text{CDCL}(\oplus)$ not only produces $\text{Res}(\oplus)$ proofs, but also polynomially simulates $\text{Res}(\oplus)$ given nondeterministic decisions and restarts, mirroring the classical relationship between CDCL and Resolution. Our key technical tool is a new set of inference rules for $\text{Res}(\oplus)$ that helps us translate Resolution-based subroutines such as 1-UIP clause learning. Altogether, $\text{CDCL}(\oplus)$'s parity reasoning includes branching on arbitrary parity equations, linear-algebraic reasoning during unit propagation, and learning linear clauses through conflict analysis. We provide a proof-of-concept implementation of $\text{CDCL}(\oplus)$ called \textsf{Xorcle}, which includes adaptations of existing CDCL heuristics to XNF formulas and an extension of LRUP proof logging that we call $\text{LRUP}(\oplus)$. On a selected suite of benchmarks focusing on native XNF formulas, \textsf{Xorcle} outperforms existing solvers such as Kissat and CryptoMiniSAT. Additionally, on Tseitin formulas written in CNF, even without preprocessing, \textsf{Xorcle}'s running time appears to scale nearly polynomially.