Solving Quantified Boolean Formulas with Few Existential Variables
The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness. Many problems of central interest in AI are in general not included in NP, e.g., planning, model checking, and non-monotonic reasoning, and for such problems QBF has successfully been used as a modelling tool. However, solvers for QBF are not as advanced as state of the art SAT solvers, which has prevented QBF from becoming a universal modelling language for PSPACE-complete problems. A theoretical explanation is that QBF (as well as many other PSPACE-complete problems) lacks natural parameters} guaranteeing fixed-parameter tractability (FPT). In this paper we tackle this problem and consider a simple but overlooked parameter: the number of existentially quantified variables. This natural parameter is virtually unexplored in the literature which one might find surprising given the general scarcity of FPT algorithms for QBF. Via this parameterization we then develop a novel FPT algorithm applicable to QBF instances in conjunctive normal form (CNF) of bounded clause length. We complement this by a W[1]-hardness result for QBF in CNF of unbounded clause length as well as sharper lower bounds for the bounded arity case under the (strong) exponential-time hypothesis.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Synthesis with Explicit Dependencies
Quantified Boolean Formulas (QBF) extend propositional logic with quantification $\forall, \exists$. In QBF, an existentially quantified variable is allowed to depend on all universally quantified variables in its scope.…
On Quantifying Literals in Boolean Logic and Its Applications to Explainable AI
Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have bee…
Game Tree Search in a Robust Multistage Optimization Framework: Exploiting Pruning Mechanisms
We investigate pruning in search trees of so-called quantified integer linear programs (QIPs). QIPs consist of a set of linear inequalities and a minimax objective function, where some variables are existentially and oth…
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.…
TranslationLearning Heuristics for Quantified Boolean Formulas through Reinforcement Learning
We demonstrate how to learn efficient heuristics for automated reasoning algorithms for quantified Boolean formulas through deep reinforcement learning. We focus on a backtracking search algorithm, which can already solv…
Deep Reinforcement Learningreinforcement-learningReinforcement LearningReinforcement Learning (RL)