Solving Quantified Boolean Formulas with Circuit Observability Don’t Cares

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.

Download Full-text

Chapter 29. Theory of Quantified Boolean Formulas

Frontiers in Artificial Intelligence and Applications - Handbook of Satisfiability ◽

10.3233/faia201013 ◽

2021 ◽

Author(s):

Hans Kleine Büning ◽

Uwe Bubeck

Keyword(s):

Normal Form ◽

Boolean Function ◽

Expressive Power ◽

Modeling Language ◽

Complex Problems ◽

Quantified Boolean Formulas ◽

Horn Formulas ◽

Boolean Formulas ◽

Function Models ◽

Resolution Calculus

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).

Download Full-text

Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems

Theory and Applications of Satisfiability Testing - Lecture Notes in Computer Science ◽

10.1007/11527695_23 ◽

2005 ◽

pp. 292-305 ◽

Cited By ~ 5

Author(s):

Daijue Tang ◽

Yinlei Yu ◽

Darsh Ranjan ◽

Sharad Malik

Keyword(s):

State Space ◽

Quantified Boolean Formulas ◽

Boolean Formulas

Download Full-text

Beyond NP: Quantifying over Answer Sets

Theory and Practice of Logic Programming ◽

10.1017/s1471068419000140 ◽

2019 ◽

Vol 19 (5-6) ◽

pp. 705-721

Author(s):

GIOVANNI AMENDOLA ◽

FRANCESCO RICCA ◽

MIROSLAW TRUSZCZYNSKI

Keyword(s):

Answer Set Programming ◽

The Other ◽

Polynomial Hierarchy ◽

Programming Paradigm ◽

Quantified Boolean Formulas ◽

Boolean Formulas ◽

The One ◽

Image Position ◽

Answer Sets ◽

Computational Properties

AbstractAnswer Set Programming (ASP) is a logic programming paradigm featuring a purely declarative language with comparatively high modeling capabilities. Indeed, ASP can model problems in NP in a compact and elegant way. However, modeling problems beyond NP with ASP is known to be complicated, on the one hand, and limited to problems in $\[\Sigma _2^P\]$ on the other. Inspired by the way Quantified Boolean Formulas extend SAT formulas to model problems beyond NP, we propose an extension of ASP that introduces quantifiers over stable models of programs. We name the new language ASP with Quantifiers (ASP(Q)). In the paper we identify computational properties of ASP(Q); we highlight its modeling capabilities by reporting natural encodings of several complex problems with applications in artificial intelligence and number theory; and we compare ASP(Q) with related languages. Arguably, ASP(Q) allows one to model problems in the Polynomial Hierarchy in a direct way, providing an elegant expansion of ASP beyond the class NP.

Download Full-text