MatSat: a matrix-based differentiable SAT solver
- URL: http://arxiv.org/abs/2108.06481v1
- Date: Sat, 14 Aug 2021 07:38:06 GMT
- Title: MatSat: a matrix-based differentiable SAT solver
- Authors: Taisuke Sato (1) and Ryosuke Kojima (2) ((1) National Institute of
Informatics (NII), (2) Graduate School of Medicine, Kyoto University)
- Abstract summary: We propose a new approach to SAT solving which solves SAT problems in vector spaces as a cost minimization problem of a non-negative differentiable cost function Jsat.
In our approach, a solution, i.e., satisfying assignment, for a SAT problem in n variables is represented by a binary vector u in 0,1n that makes Jsat(u) zero.
We implement our approach as a matrix-based differential SAT solver MatSat.
- Score: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We propose a new approach to SAT solving which solves SAT problems in vector
spaces as a cost minimization problem of a non-negative differentiable cost
function J^sat. In our approach, a solution, i.e., satisfying assignment, for a
SAT problem in n variables is represented by a binary vector u in {0,1}^n that
makes J^sat(u) zero. We search for such u in a vector space R^n by cost
minimization, i.e., starting from an initial u_0 and minimizing J to zero while
iteratively updating u by Newton's method. We implemented our approach as a
matrix-based differential SAT solver MatSat. Although existing main-stream SAT
solvers decide each bit of a solution assignment one by one, be they of
conflict driven clause learning (CDCL) type or of stochastic local search (SLS)
type, MatSat fundamentally differs from them in that it continuously approach a
solution in a vector space. We conducted an experiment to measure the
scalability of MatSat with random 3-SAT problems in which MatSat could find a
solution up to n=10^5 variables. We also compared MatSat with four
state-of-the-art SAT solvers including winners of SAT competition 2018 and SAT
Race 2019 in terms of time for finding a solution, using a random benchmark set
from SAT 2018 competition and an artificial random 3-SAT instance set. The
result shows that MatSat comes in second in both test sets and outperforms all
the CDCL type solvers.
Related papers
- General Method for Solving Four Types of SAT Problems [12.28597116379225]
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.
arXiv Detail & Related papers (2023-12-27T06:09:48Z) - 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) - Near-Optimal Bounds for Learning Gaussian Halfspaces with Random
Classification Noise [50.64137465792738]
We show that any efficient SQ algorithm for the problem requires sample complexity at least $Omega(d1/2/(maxp, epsilon)2)$.
Our lower bound suggests that this quadratic dependence on $1/epsilon$ is inherent for efficient algorithms.
arXiv Detail & Related papers (2023-07-13T18:59: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) - Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
We propose AsymSAT, a GNN-based architecture which integrates recurrent neural networks to generate dependent predictions for variable assignments.
Experiment results show that dependent variable prediction extends the solving capability of the GNN-based method as it improves the number of solved SAT instances on large test sets.
arXiv Detail & Related papers (2023-04-18T05:33:33Z) - 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) - 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) - NLocalSAT: Boosting Local Search with Solution Prediction [36.69915361918781]
An effective way for solving a satisfiable SAT problem is the local search (SLS)
This method is assigned in a random manner, which impacts the effectiveness of SLS solvers.
NLocalSAT combines SLS with a solution prediction model, which boosts SLS by changing initialization assignments with a neural network.
Experiments show that solvers with NLocalSAT achieve 27% 62% improvement over the original SLS solvers.
arXiv Detail & Related papers (2020-01-26T04:22:53Z)
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.