General Method for Solving Four Types of SAT Problems
- URL: http://arxiv.org/abs/2312.16423v1
- Date: Wed, 27 Dec 2023 06:09:48 GMT
- Title: General Method for Solving Four Types of SAT Problems
- Authors: Anqi Li and Congying Han and Tiande Guo and Haoran Li and Bonan Li
- Abstract summary: Existing methods provide varying algorithms for different types of Boolean satisfiability problems (SAT)
This study proposes a unified framework DCSAT based on integer programming and reinforcement learning (RL) algorithm to solve different types of SAT problems.
- Score: 12.28597116379225
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Existing methods provide varying algorithms for different types of Boolean
satisfiability problems (SAT), lacking a general solution framework.
Accordingly, this study proposes a unified framework DCSAT based on integer
programming and reinforcement learning (RL) algorithm to solve different types
of SAT problems such as MaxSAT, Weighted MaxSAT, PMS, WPMS. Specifically, we
first construct a consolidated integer programming representation for four
types of SAT problems by adjusting objective function coefficients. Secondly,
we construct an appropriate reinforcement learning models based on the 0-1
integer programming for SAT problems. Based on the binary tree search
structure, we apply the Monte Carlo tree search (MCTS) method on SAT problems.
Finally, we prove that this method can find all optimal Boolean assignments
based on Wiener-khinchin law of large Numbers. We experimentally verify that
this paradigm can prune the unnecessary search space to find the optimal
Boolean assignments for the problem. Furthermore, the proposed method can
provide diverse labels for supervised learning methods for SAT problems.
Related papers
- Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
We introduce the notion of decomposition hardness (d-hardness)
We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
arXiv Detail & Related papers (2023-12-16T12:44:36Z) - Machine Learning for SAT: Restricted Heuristics and New Graph
Representations [0.8870188183999854]
SAT is a fundamental NP-complete problem with many applications, including automated scheduling.
To solve large instances, SAT solvers have to rely on Booleans, e.g., choosing a branching variable in DPLL and CDCL solvers.
We suggest a strategy of making a few initial steps with a trained ML model and then releasing control to classical runtimes.
arXiv Detail & Related papers (2023-07-18T10:46:28Z) - A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
This paper presents and describes a hybrid quantum computing strategy for solving 3-SAT problems.
The performance of this approximation has been tested over a set of representative scenarios when dealing with 3-SAT from the quantum computing perspective.
arXiv Detail & Related papers (2023-06-07T12:19:22Z) - Evolutionary Diversity Optimisation in Constructing Satisfying
Assignments [20.386139395296215]
This paper studies the Boolean satisfiability problem (SAT) in the context of EDO.
SAT is of great importance in computer science and differs from the other problems studied in EDO literature, such as KP and TSP.
We introduce evolutionary algorithms employing a well-known SAT solver to maximise diversity among a set of SAT solutions explicitly.
arXiv Detail & Related papers (2023-05-19T06:26:10Z) - Estimating the hardness of SAT encodings for Logical Equivalence
Checking of Boolean circuits [58.83758257568434]
We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning.
The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
arXiv Detail & Related papers (2022-10-04T09:19:13Z) - SATformer: Transformer-Based UNSAT Core Learning [0.0]
This paper introduces SATformer, a Transformer-based approach for the Boolean Satisfiability (SAT) problem.
Rather than solving the problem directly, SATformer approaches the problem from the opposite direction by focusing on unsatisfiability.
SATformer is trained through a multi-task learning approach, using the single-bit satisfiability result and the minimal unsatisfiable core.
Experimental results show that our SATformer can decrease the runtime of existing solvers by an average of 21.33%.
arXiv Detail & Related papers (2022-09-02T11:17:39Z) - DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
We present DeepSAT, a novel end-to-end learning framework for the Boolean satisfiability (SAT) problem.
DeepSAT achieves significant accuracy improvements over state-of-the-art learning-based SAT solutions.
arXiv Detail & Related papers (2022-05-27T03:20:42Z) - Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques.
We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
arXiv Detail & Related papers (2022-03-02T05:14:12Z) - 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) - Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
We propose the setting of extreme algorithm selection (XAS) where we consider fixed sets of thousands of candidate algorithms.
We assess the applicability of state-of-the-art AS techniques to the XAS setting and propose approaches leveraging a dyadic feature representation.
arXiv Detail & Related papers (2020-01-29T09:40:58Z)
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.