DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving
- URL: http://arxiv.org/abs/2205.03747v2
- Date: Sun, 7 May 2023 02:52:07 GMT
- Title: DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving
- Authors: Anastasios Kyrillidis, Moshe Y. Vardi, Zhiwei Zhang
- Abstract summary: We propose a novel dynamic-programming approach for solving generalized MaxSAT problems with hybrid constraints.
Our versatile framework admits many generalizations of CNF-MaxSAT, such as MaxSAT, Min-MaxSAT, and MinSAT with hybrid constraints.
Empirical results indicate that DPMS is able to solve certain problems quickly, where other algorithms based on various techniques all fail.
- Score: 45.21499915442282
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Boolean MaxSAT, as well as generalized formulations such as Min-MaxSAT and
Max-hybrid-SAT, are fundamental optimization problems in Boolean reasoning.
Existing methods for MaxSAT have been successful in solving benchmarks in CNF
format. They lack, however, the ability to handle 1) (non-CNF) hybrid
constraints, such as XORs and 2) generalized MaxSAT problems natively. To
address this issue, we propose a novel dynamic-programming approach for solving
generalized MaxSAT problems with hybrid constraints -- called
\emph{Dynamic-Programming-MaxSAT} or DPMS for short -- based on Algebraic
Decision Diagrams (ADDs). With the power of ADDs and the (graded)
project-join-tree builder, our versatile framework admits many generalizations
of CNF-MaxSAT, such as MaxSAT, Min-MaxSAT, and MinSAT with hybrid constraints.
Moreover, DPMS scales provably well on instances with low width. Empirical
results indicate that DPMS is able to solve certain problems quickly, where
other algorithms based on various techniques all fail. Hence, DPMS is a
promising framework and opens a new line of research that invites more
investigation in the future.
Related papers
- Certified MaxSAT Preprocessing [9.717669529984349]
MaxSAT has become a viable approach for solving NP-hard optimization problems.
ensuring correctness of MaxSAT solvers has remained an important concern.
We show how pseudo-Boolean proof logging can be used to certify the correctness of a range of modern MaxSAT preprocessing techniques.
arXiv Detail & Related papers (2024-04-26T10:55:06Z) - SEGO: Sequential Subgoal Optimization for Mathematical Problem-Solving [64.38649623473626]
Large Language Models (LLMs) have driven substantial progress in artificial intelligence.
We propose a novel framework called textbfSEquential subtextbfGoal textbfOptimization (SEGO) to enhance LLMs' ability to solve mathematical problems.
arXiv Detail & Related papers (2023-10-19T17:56:40Z) - UpMax: User partitioning for MaxSAT [2.2022484178680872]
partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms.
This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms.
arXiv Detail & Related papers (2023-05-25T15:50:00Z) - Decentralized Riemannian Algorithm for Nonconvex Minimax Problems [82.50374560598493]
The minimax algorithms for neural networks have been developed to solve many problems.
In this paper, we propose two types of minimax algorithms.
For the setting, we propose DRSGDA and prove that our method achieves a gradient.
arXiv Detail & Related papers (2023-02-08T01:42:45Z) - Constrained mixers for the quantum approximate optimization algorithm [55.41644538483948]
We present a framework for constructing mixing operators that restrict the evolution to a subspace of the full Hilbert space.
We generalize the "XY"-mixer designed to preserve the subspace of "one-hot" states to the general case of subspaces given by a number of computational basis states.
Our analysis also leads to valid Trotterizations for "XY"-mixer with fewer CX gates than is known to date.
arXiv Detail & Related papers (2022-03-11T17:19:26Z) - BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit [16.371916145216737]
We propose a local search algorithm called BandMaxSAT, that applies a multi-armed bandit to guide the search direction.
Extensive experiments demonstrate that BandMaxSAT significantly outperforms the state-of-the-art (W)PMS local search algorithm SATLike3.0.
The resulting solver BandMaxSAT-c also outperforms some of the best state-of-the-art complete (W)PMS solvers, including SATLike-c, Loandra and TT-Open-WBO-Inc.
arXiv Detail & Related papers (2022-01-14T16:32:39Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems.
In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
arXiv Detail & Related papers (2021-07-15T04:47:35Z) - Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length.
This problem is central in Combinatorial Testing for the detection of system failures.
arXiv Detail & Related papers (2021-05-26T14:00:56Z) - Fault Tree Analysis: Identifying Maximum Probability Minimal Cut Sets
with MaxSAT [0.342658286826597]
We model the MPMCS problem as a weighted Partial MaxSAT problem and solve it using a parallel SAT-solving architecture.
The results obtained with our open source tool indicate that the approach is effective and efficient.
arXiv Detail & Related papers (2020-05-05T19:47:15Z) - Hardness of Random Optimization Problems for Boolean Circuits,
Low-Degree Polynomials, and Langevin Dynamics [78.46689176407936]
We show that families of algorithms fail to produce nearly optimal solutions with high probability.
For the case of Boolean circuits, our results improve the state-of-the-art bounds known in circuit complexity theory.
arXiv Detail & Related papers (2020-04-25T05:45:59Z)
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.