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

• IGMaxHS -- An Incremental MaxSAT Solver with Support for XOR Clauses [0.0]
  We introduce IGMaxHS, which is based on the solvers iMaxHS and GaussMaxHS, but poses fewer restrictions on the XOR constraints than GaussMaxHS. IGMaxHS is the only solver that reported neither incorrect unsatisfiability verdicts nor invalid models nor incoherent cost model combinations. We show that IGMaxHS is capable of decoding quantum color codes through simulation with the Munich Quantum Toolkit.
  arXiv  Detail & Related papers  (2024-10-21T11:21:21Z)
• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  The framework combines Monte Carlo Tree Search (MCTS) with iterative Self-Refine to optimize the reasoning path. The framework has been tested on general and advanced benchmarks, showing superior performance in terms of search efficiency and problem-solving capability.
  arXiv  Detail & Related papers  (2024-10-03T18:12:29Z)
• 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)
• 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)
• 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)

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.