General Boolean Formula Minimization with QBF Solvers
- URL: http://arxiv.org/abs/2303.06643v1
- Date: Sun, 12 Mar 2023 12:08:58 GMT
- Title: General Boolean Formula Minimization with QBF Solvers
- Authors: Eduardo Cal\`o, Jordi Levy
- Abstract summary: 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.
- Score: 4.264192013842096
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The minimization of propositional formulae is a classical problem in logic,
whose first algorithms date back at least to the 1950s with the works of Quine
and Karnaugh. Most previous work in the area has focused on obtaining minimal,
or quasi-minimal, formulae in conjunctive normal form (CNF) or disjunctive
normal form (DNF), with applications in hardware design. In this paper, we are
interested in the problem of obtaining an equivalent formula in any format,
also allowing connectives that are not present in the original formula. We are
primarily motivated in applying minimization algorithms to generate natural
language translations of the original formula, where using shorter equivalents
as input may result in better translations. Recently, Buchfuhrer and Umans have
proved that the (decisional version of the) problem is $\Sigma_2^p$-complete.
We analyze three possible (practical) approaches to solving the problem.
First, using brute force, generating all possible formulae in increasing size
and checking if they are equivalent to the original formula by testing all
possible variable assignments. Second, generating the Tseitin coding of all the
formulae and checking equivalence with the original using a SAT solver. Third,
encoding the problem as a Quantified Boolean Formula (QBF), and using a QBF
solver. Our results show that the QBF approach largely outperforms the other
two.
Related papers
- Solving Quantified Boolean Formulas with Few Existential Variables [19.221715574358207]
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.
arXiv Detail & Related papers (2024-05-10T14:07:29Z) - A Framework to Formulate Pathfinding Problems for Quantum Computing [2.9723999564214267]
We propose a framework to automatically generate QUBO formulations for pathfinding problems.
It supports three different encoding schemes that can easily be compared without requiring manual reformulation efforts.
The resulting QUBO formulations are robust and efficient, reducing the previously tedious and error-prone reformulation process.
arXiv Detail & Related papers (2024-04-16T18:00:06Z) - Synthesising Recursive Functions for First-Order Model Counting:
Challenges, Progress, and Conjectures [12.47276164048813]
First-order model counting (FOMC) is a computational problem that asks to count the models of a sentence in finite-domain first-order logic.
We relax the restrictions that typically accompany domain recursion to work with directed graphs that may contain cycles.
These improvements allow the algorithm to find efficient solutions to counting problems that were previously beyond its reach.
arXiv Detail & Related papers (2023-06-07T06:49:01Z) - Quantum Worst-Case to Average-Case Reductions for All Linear Problems [66.65497337069792]
We study the problem of designing worst-case to average-case reductions for quantum algorithms.
We provide an explicit and efficient transformation of quantum algorithms that are only correct on a small fraction of their inputs into ones that are correct on all inputs.
arXiv Detail & Related papers (2022-12-06T22:01:49Z) - 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) - Dynamic programming by polymorphic semiring algebraic shortcut fusion [1.9405875431318445]
Dynamic programming (DP) is an algorithmic design paradigm for the efficient, exact solution of intractable, problems.
This paper presents a rigorous algebraic formalism for systematically deriving DP algorithms, based on semiring.
arXiv Detail & Related papers (2021-07-05T00:51:02Z) - Bayesian Algorithm Execution: Estimating Computable Properties of
Black-box Functions Using Mutual Information [78.78486761923855]
In many real world problems, we want to infer some property of an expensive black-box function f, given a budget of T function evaluations.
We present a procedure, InfoBAX, that sequentially chooses queries that maximize mutual information with respect to the algorithm's output.
On these problems, InfoBAX uses up to 500 times fewer queries to f than required by the original algorithm.
arXiv Detail & Related papers (2021-04-19T17:22:11Z) - Boosting Data Reduction for the Maximum Weight Independent Set Problem
Using Increasing Transformations [59.84561168501493]
We introduce new generalized data reduction and transformation rules for the maximum weight independent set problem.
Surprisingly, these so-called increasing transformations can simplify the problem and also open up the reduction space to yield even smaller irreducible graphs later in the algorithm.
Our algorithm computes significantly smaller irreducible graphs on all except one instance, solves more instances to optimality than previously possible, is up to two orders of magnitude faster than the best state-of-the-art solver, and finds higher-quality solutions than solvers DynWVC and HILS.
arXiv Detail & Related papers (2020-08-12T08:52:50Z) - Strong Generalization and Efficiency in Neural Programs [69.18742158883869]
We study the problem of learning efficient algorithms that strongly generalize in the framework of neural program induction.
By carefully designing the input / output interfaces of the neural model and through imitation, we are able to learn models that produce correct results for arbitrary input sizes.
arXiv Detail & Related papers (2020-07-07T17:03:02Z) - Sparse Hashing for Scalable Approximate Model Counting: Theory and
Practice [36.8421113576893]
Given a CNF formula F on n variables, the problem of model counting or #SAT is to compute the number of satisfying assignments of F.
Recent years have witnessed a surge of effort towards developing efficient algorithmic techniques.
arXiv Detail & Related papers (2020-04-30T11:17:26Z) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
A fundamental component of neural network verification is the computation of bounds on the values their outputs can take.
We propose a novel approach based on Lagrangian Decomposition.
We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
arXiv Detail & Related papers (2020-02-24T17:55:10Z)
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.