Planning with Incomplete Information in Quantified Answer Set Programming

We present a general approach to planning with incomplete information in Answer Set Programming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptions. We represent planning problems using a simple formalism where logic programs describe the transition function between states, the initial states and the goal states. For solving planning problems, we use Quantified Answer Set Programming (QASP), an extension of ASP with existential and universal quantifiers over atoms that is analogous to Quantified Boolean Formulas (QBFs). We define the language of quantified logic programs and use it to represent the solutions different variants of conformant and conditional planning. On the practical side, we present a translation-based QASP solver that converts quantified logic programs into QBFs and then executes a QBF solver, and we evaluate experimentally the approach on conformant and conditional planning benchmarks.

Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations

In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) for obtaining a propositional abstraction of the QBF. If this formula is false, the truth value of the QBF is decided, otherwise further refinement steps are necessary. Classically, expansion-based solvers process the given formula quantifier-block wise and use one SAT solver per quantifier block. In this paper, we present a novel algorithm for expansion-based QBF solving that deals with the whole quantifier prefix at once. Hence recursive applications of the expansion principle are avoided and only two incremental SAT solvers are required. While our algorithm is naturally based on the $$\forall $$ ∀ Exp+Res calculus that is the formal foundation of expansion-based solving, it is conceptually simpler than present recursive approaches. Experiments indicate that the performance of our simple approach is comparable with the state of the art of QBF solving, especially in combination with other solving techniques.

Program Synthesis as Dependency Quantified Formula Modulo Theory

Given a specification φ(X, Y ) over inputs X and output Y and defined over a background theory T, the problem of program synthesis is to design a program f such that Y = f (X), satisfies the specification φ. Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominant approach to program synthesis where in addition to the specification φ, the end-user also specifies a grammar L to aid the underlying synthesis engine. This paper investigates the feasibility of synthesis techniques without grammar, a sub-class defined as T constrained synthesis. We show that T-constrained synthesis can be reduced to DQF(T),i.e., to the problem of finding a witness of a dependency quantified formula modulo theory. When the underlying theory is the theory of bitvectors, the corresponding DQF problem can be further reduced to Dependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBF solving to design DQBF-based synthesizers that outperform the domain-specific program synthesis techniques; thereby positioning DQBF as a core representation language for program synthesis. Our empirical analysis shows that T-constrained synthesis can achieve significantly better performance than syntax-guided approaches. Furthermore, the general-purpose DQBF solvers perform on par with domain-specific synthesis techniques.

Chapter 31. Quantified Boolean Formulas

Solvers for quantified Boolean formulas (QBF) have become powerful tools for tackling hard computational problems from various application domains, even beyond the scope of SAT. This chapter gives a description of the main algorithmic paradigms for QBF solving, including quantified conflict driven clause learning (QCDCL), expansion-based solving, dependency schemes, and QBF preprocessing. Particular emphasis is laid on the connections of these solving approaches to QBF proof systems: Q-Resolution and its variants in the case of QCDCL, expansion QBF resolution calculi for expansion-based solving, and QRAT for preprocessing. The chapter also surveys the relations between the various QBF proof systems and results on their proof complexity, thereby shedding light on the diverse performance characteristics of different solving approaches that are observed in practice.

Chapter 29. Theory of Quantified Boolean Formulas

Quantified Boolean formulas (QBF) are a generalization of propositional formulas by allowing universal and existential quantifiers over variables. This enhancement makes QBF a concise and natural modeling language in which problems from many areas, such as planning, scheduling or verification, can often be encoded in a more compact way than with propositional formulas. We introduce in this chapter the syntax and semantics of QBF and present fundamental concepts. This includes normal form transformations and Q-resolution, an extension of the propositional resolution calculus. In addition, Boolean function models are introduced to describe the valuation of formulas and the behavior of the quantifiers. We also discuss the expressive power of QBF and provide an overview of important complexity results. These illustrate that the greater capabilities of QBF lead to more complex problems, which makes it interesting to consider suitable subclasses of QBF. In particular, we give a detailed look at quantified Horn formulas (QHORN) and quantified 2-CNF (Q2-CNF).

Chapter 14. Minimal Unsatisfiability and Autarkies

Minimal unsatisfiability describes the reduced kernel of unsatisfiable formulas. The investigation of this property is very helpful in understanding the reasons for unsatisfiability as well as the behaviour of SAT-solvers and proof calculi. Moreover, for propositional formulas and quantified Boolean formulas the computational complexity of various SAT-related problems are strongly related to the complexity of minimal unsatisfiable formulas. While “minimal unsatisfiability” studies the structure of problem instances without redundancies, the study of “autarkies” considers the redundancies themselves, in various guises related to partial assignments which satisfy some part of the problem instance while leaving the rest “untouched”. As it turns out, autarky theory creates many bridges to combinatorics, algebra and logic, and the second part of this chapter provides a solid foundation of the basic ideas and results of autarky theory: the basic algorithmic problems, the algebra involved, and relations to various combinatorial theories (e.g., matching theory, linear programming, graph theory, the theory of permanents). Also the general theory of autarkies as a kind of combinatorial “meta theory” is sketched (regarding its basic notions).

Chapter 30. Reasoning with Quantified Boolean Formulas

The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas(QBFs) is an important research issue in Artificial Intelligence and Computer Science. Indeed, QBF solvers have already been proposed for many reasoning tasks in knowledge representation and reasoning, in automated planning and in formal methods for computer aided design. Even more, since QBF reasoning is the prototypical PSPACE problem, the reduction of many other decision problems in PSPACE are readily available. For these reasons, in the last few years several decision procedures for QBFs have been proposed and implemented, mostly based either on search or on variable elimination, or on a combination of the two. In this chapter, after a brief recap of the basic terminology and notation about QBFs, we briefly review various applications of QBF reasoning that have been recently proposed, and then we focus on the description of the main approaches which are at the basis of currently available solvers for prenex QBFs in conjunctive normal form (CNF). Other approaches and extensions to non prenex, non CNF QBFs are briefly reviewed at the end of the chapter.

Dual Proof Generation for Quantified Boolean Formulas with a BDD-based Solver

Existing proof-generating quantified Boolean formula (QBF) solvers must construct a different type of proof depending on whether the formula is false (refutation) or true (satisfaction). We show that a QBF solver based on ordered binary decision diagrams (BDDs) can emit a single dual proof as it operates, supporting either outcome. This form consists of a sequence of equivalence-preserving clause addition and deletion steps in an extended resolution framework. For a false formula, the proof terminates with the empty clause, indicating conflict. For a true one, it terminates with all clauses deleted, indicating tautology. Both the length of the proof and the time required to check it are proportional to the total number of BDD operations performed. We evaluate our solver using a scalable benchmark based on a two-player tiling game.

Fixed-Parameter Tractability of Dependency QBF with Structural Parameters

We study dependency quantified Boolean formulas (DQBF), an extension of QBF in which dependencies of existential variables are listed explicitly rather than being implicit in the order of quantifiers. DQBF evaluation is a canonical NEXPTIME-complete problem, a complexity class containing many prominent problems that arise in Knowledge Representation and Reasoning. One approach for solving such hard problems is to identify and exploit structural properties captured by numerical parameters such that bounding these parameters gives rise to an efficient algorithm. This idea is captured by the notion of fixed-parameter tractability (FPT). We initiate the study of DQBF through the lens of fixed-parameter tractability and show that the evaluation problem becomes FPT under two natural parameterizations: the treewidth of the primal graph of the DQBF instance combined with a restriction on the interactions between the dependency sets, and also the treedepth of the primal graph augmented by edges representing dependency sets.

Controllability of Control Argumentation Frameworks

Control argumentation frameworks (CAFs) allow for modeling uncertainties inherent in various argumentative settings. We establish a complete computational complexity map of the central computational problem of controllability in CAFs for five key semantics. We also develop Boolean satisfiability based counterexample-guided abstraction refinement algorithms and direct encodings of controllability as quantified Boolean formulas, and empirically evaluate their scalability on a range of NP-hard variants of controllability.