scholarly journals iDQ: Instantiation-Based DQBF Solving

10.29007/1s5k ◽  
2018 ◽  
Author(s):  
Andreas Fröhlich ◽  
Gergely Kovásznai ◽  
Armin Biere ◽  
Helmut Veith
Keyword(s):  
Experimental Analysis ◽  
Theoretical Foundation ◽  
Practical Applications ◽  
Quantified Boolean Formulas ◽  
Boolean Formulas ◽  
Henkin Quantifiers

Dependency Quantified Boolean Formulas (DQBF) are obtained by adding Henkin quantifiers to Boolean formulas and have seen growing interest in the last years. Since deciding DQBF is NEXPTIME-complete, efficient ways of solving it would have many practical applications. Still, there is only few work on solving this kind of formulas in practice. In this paper, we present an instantiation-based technique to solve DQBF efficiently. Apart from providing a theoretical foundation, we also propose a concrete implementation of our algorithm. Finally, we give a detailed experimental analysis evaluating our prototype iDQ on several DQBF as well as QBF benchmarks.

Analysis of Incomplete Circuits Using Dependency Quantified Boolean Formulas

2017 ◽  
pp. 151-168 ◽  
Author(s):  
Ralf Wimmer ◽  
Karina Wimmer ◽  
Christoph Scholl ◽  
Bernd Becker
Keyword(s):  
Quantified Boolean Formulas ◽  
Boolean Formulas

Chapter 31. Quantified Boolean Formulas

2021 ◽  
Author(s):  
Olaf Beyersdorff ◽  
Mikoláš Janota ◽  
Florian Lonsing ◽  
Martina Seidl
Keyword(s):  
Performance Characteristics ◽  
Proof Complexity ◽  
Proof Systems ◽  
Quantified Boolean Formulas ◽  
Boolean Formulas ◽  
Clause Learning ◽  
Dependency Schemes

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

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

Sign in / Sign up

Export Citation Format

Share Document