W2SAT: Learning to generate SAT instances from Weighted Literal
Incidence Graphs
- URL: http://arxiv.org/abs/2302.00272v1
- Date: Wed, 1 Feb 2023 06:30:41 GMT
- Title: W2SAT: Learning to generate SAT instances from Weighted Literal
Incidence Graphs
- Authors: Weihuang Wen, Tianshu Yu
- Abstract summary: W2SAT is a framework to generate SAT formulas by learning intrinsic structures and properties from given real-world/industrial instances.
We introduce a novel SAT representation called Weighted Literal Incidence Graph (WLIG), which exhibits strong representation ability and generalizability.
Decoding from WLIG into SAT problems is then modeled as finding overlapping cliques with a novel hill-climbing optimization method.
- Score: 13.173307471333619
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The Boolean Satisfiability (SAT) problem stands out as an attractive
NP-complete problem in theoretic computer science and plays a central role in a
broad spectrum of computing-related applications. Exploiting and tuning SAT
solvers under numerous scenarios require massive high-quality industry-level
SAT instances, which unfortunately are quite limited in the real world. To
address the data insufficiency issue, in this paper, we propose W2SAT, a
framework to generate SAT formulas by learning intrinsic structures and
properties from given real-world/industrial instances in an implicit fashion.
To this end, we introduce a novel SAT representation called Weighted Literal
Incidence Graph (WLIG), which exhibits strong representation ability and
generalizability against existing counterparts, and can be efficiently
generated via a specialized learning-based graph generative model. Decoding
from WLIGs into SAT problems is then modeled as finding overlapping cliques
with a novel hill-climbing optimization method termed Optimal Weight Coverage
(OWC). Experiments demonstrate the superiority of our WLIG-induced approach in
terms of graph metrics, efficiency, and scalability in comparison to previous
methods. Additionally, we discuss the limitations of graph-based SAT generation
for real-world applications, especially when utilizing generated instances for
SAT solver parameter-tuning, and pose some potential directions.
Related papers
- GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
We present GraSS, a novel approach for automatic SAT solver selection based on tripartite graph representations of instances.
We enrich the graph representation with domain-specific decisions, such as novel node feature design.
We demonstrate that this combination of raw representations and domain-specific choices leads to improvements in runtime.
arXiv Detail & Related papers (2024-05-17T18:00:50Z) - Using deep learning to construct stochastic local search SAT solvers
with performance bounds [0.0]
We train oracles using Graph Neural Networks and evaluate them on two SLS solvers on random SAT instances of varying difficulty.
We find that access to GNN-based oracles significantly boosts the performance of both solvers.
arXiv Detail & Related papers (2023-09-20T16:27:52Z) - 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) - SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs)
We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer.
We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
arXiv Detail & Related papers (2023-05-16T17:55:51Z) - 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) - 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)
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.