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

• Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling [90.86991492288487]
  evaluating constraint on every token can be prohibitively expensive. LCD can distort the global distribution over strings, sampling tokens based only on local information. We show that our approach is superior to state-of-the-art baselines.
  arXiv  Detail & Related papers  (2025-04-07T18:30:18Z)
• Explicit Solution Equation for Every Combinatorial Problem via Tensor Networks: MeLoCoToN [55.2480439325792]
  We show that every computation problem has an exact explicit equation that returns its solution. We present a method to obtain an equation that solves exactly any problem, both inversion, constraint satisfaction and optimization.
  arXiv  Detail & Related papers  (2025-02-09T18:16:53Z)
• Simple and Provable Scaling Laws for the Test-Time Compute of Large Language Models [70.07661254213181]
  We propose two principled algorithms for the test-time compute of large language models. We prove theoretically that the failure probability of one algorithm decays to zero exponentially as its test-time compute grows.
  arXiv  Detail & Related papers  (2024-11-29T05:29:47Z)
• Neural Algorithmic Reasoning with Multiple Correct Solutions [16.045068056647676]
  In some applications, it is desirable to recover more than one correct solution. We demonstrate our method on two classical algorithms: Bellman-Ford (BF) and Depth-First Search (DFS) This method involves generating appropriate training data as well as sampling and validating solutions from model output.
  arXiv  Detail & Related papers  (2024-09-11T02:29:53Z)
• An encoding of argumentation problems using quadratic unconstrained binary optimization [1.104960878651584]
  We develop a way to encode several NP-Complete problems in Abstract Argumentation to Quadratic Unconstrained Binary Optimization problems. With the QUBO formulation, exploiting new computing architectures, such as Quantum and Digital Annealers, is possible. We performed tests to prove the correctness and applicability of classical problems in Argumentation and enforcement of argument sets.
  arXiv  Detail & Related papers  (2024-09-09T11:29:46Z)
• Sum-of-Squares inspired Quantum Metaheuristic for Polynomial Optimization with the Hadamard Test and Approximate Amplitude Constraints [76.53316706600717]
  Recently proposed quantum algorithm arXiv:2206.14999 is based on semidefinite programming (SDP) We generalize the SDP-inspired quantum algorithm to sum-of-squares. Our results show that our algorithm is suitable for large problems and approximate the best known classicals.
  arXiv  Detail & Related papers  (2024-08-14T19:04:13Z)
• 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)
• 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)
• 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.