Solving Quantified Boolean Formulas with Few Existential Variables
- URL: http://arxiv.org/abs/2405.06485v1
- Date: Fri, 10 May 2024 14:07:29 GMT
- Title: Solving Quantified Boolean Formulas with Few Existential Variables
- Authors: Leif Eriksson, Victor Lagerkvist, George Osipov, Sebastian Ordyniak, Fahad Panolan, Mateusz Rychlicki,
- Abstract summary: The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness.
In this paper we consider a simple but overlooked parameter: the number of existentially quantified variables.
We then develop a novel FPT algorithm applicable to QBF instances in conjunctive normal form (CNF) of bounded clause length.
- Score: 19.221715574358207
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
Related papers
- Learning Solution-Aware Transformers for Efficiently Solving Quadratic Assignment Problem [27.33966993065248]
This work focuses on learning-based solutions for efficiently solving the Quadratic Assignment Problem (QAPs)
Current research on QAPs suffer from limited scale and inefficiency.
We propose the first solution of its kind for QAP in the learn-to-improve category.
arXiv Detail & Related papers (2024-06-14T10:15:03Z) - Reverse em-problem based on Bregman divergence and its application to classical and quantum information theory [53.64687146666141]
Recent paper introduced an analytical method for calculating the channel capacity without the need for iteration.
We turn our attention to the reverse em-problem, proposed by Toyota.
We derive a non-iterative formula for the reverse em-problem.
arXiv Detail & Related papers (2024-03-14T10:20:28Z) - Where the Really Hard Quadratic Assignment Problems Are: the QAP-SAT
instances [0.0]
The Quadratic Assignment Problem (QAP) is one of the major domains in the field of evolutionary computation optimization.
This paper studies the phase transition of the QAP, which can be described as a dramatic change in the problem's computational complexity and satisfiability.
arXiv Detail & Related papers (2024-03-05T08:56:30Z) - General Boolean Formula Minimization with QBF Solvers [4.264192013842096]
We are interested in the problem of obtaining an equivalent formula in any format.
We are motivated in applying minimization algorithms to generate natural language translations of the original formula.
We analyze three possible (practical) approaches to solving the problem.
arXiv Detail & Related papers (2023-03-12T12:08:58Z) - Symmetric Tensor Networks for Generative Modeling and Constrained
Combinatorial Optimization [72.41480594026815]
Constrained optimization problems abound in industry, from portfolio optimization to logistics.
One of the major roadblocks in solving these problems is the presence of non-trivial hard constraints which limit the valid search space.
In this work, we encode arbitrary integer-valued equality constraints of the form Ax=b, directly into U(1) symmetric networks (TNs) and leverage their applicability as quantum-inspired generative models.
arXiv Detail & Related papers (2022-11-16T18:59:54Z) - Complexity-Theoretic Limitations on Quantum Algorithms for Topological
Data Analysis [59.545114016224254]
Quantum algorithms for topological data analysis seem to provide an exponential advantage over the best classical approach.
We show that the central task of TDA -- estimating Betti numbers -- is intractable even for quantum computers.
We argue that an exponential quantum advantage can be recovered if the input data is given as a specification of simplices.
arXiv Detail & Related papers (2022-09-28T17:53:25Z) - Optimal Solutions for Joint Beamforming and Antenna Selection: From
Branch and Bound to Machine Learning [47.10315221141495]
This work revisits the joint beamforming (BF) and antenna selection (AS) problem, as well as its robust beamforming (RBF) version under imperfect channel state information (CSI)
The main contribution of this work is threefold. First, an effective it branch and bound (B&B) framework for solving the problems of interest is proposed.
Second, to expedite the potentially costly B&B algorithm, a machine learning (ML)-based scheme is proposed to help skip intermediate states of the B&B search tree.
arXiv Detail & Related papers (2022-06-11T17:43:02Z) - Hyperparameter-free deep active learning for regression problems via
query synthesis [5.572747615014008]
We propose the first DAL query-synthesis approach for regression problems.
We use the recently-proposed neural-adjoint (NA) solver to efficiently find points in the continuous input domain.
We find that NA-QBC achieves better average performance than random sampling on every benchmark problem.
arXiv Detail & Related papers (2022-01-29T18:41:08Z) - TAT-QA: A Question Answering Benchmark on a Hybrid of Tabular and
Textual Content in Finance [71.76018597965378]
We build a new large-scale Question Answering dataset containing both Tabular And Textual data, named TAT-QA.
We propose a novel QA model termed TAGOP, which is capable of reasoning over both tables and text.
arXiv Detail & Related papers (2021-05-17T06:12:06Z) - Q-Match: Iterative Shape Matching via Quantum Annealing [64.74942589569596]
Finding shape correspondences can be formulated as an NP-hard quadratic assignment problem (QAP)
This paper proposes Q-Match, a new iterative quantum method for QAPs inspired by the alpha-expansion algorithm.
Q-Match can be applied for shape matching problems iteratively, on a subset of well-chosen correspondences, allowing us to scale to real-world problems.
arXiv Detail & Related papers (2021-05-06T17:59:38Z) - Bayesian Probabilistic Numerical Integration with Tree-Based Models [5.353941016039247]
BQ is a method for solving numerical integration problems in a Bayesian manner.
BART-Int. BART priors are easy to tune and well-suited for discontinuous functions.
arXiv Detail & Related papers (2020-06-09T16:04:00Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.