AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
- URL: http://arxiv.org/abs/2402.10705v2
- Date: Fri, 31 May 2024 11:38:00 GMT
- Title: AutoSAT: Automatically Optimize SAT Solvers via Large Language Models
- Authors: Yiwen Sun, Xianyin Zhang, Shiyu Huang, Shaowei Cai, BingZhen Zhang, Ke Wei,
- Abstract summary: We present AutoSAT, a novel framework for automatically optimizing SAT solvers.
AutoSAT is based on Large Language Models (LLMs) which is able to autonomously generate codes.
AutoSAT operates on a plug-and-play basis, eliminating the need for extensive enterprise and model training.
- Score: 10.87846542244079
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Heuristics are crucial in SAT solvers, but no heuristic rules are suitable for all SAT problems. Therefore, it is helpful to refine specific heuristics for specific problems. In this context, we present AutoSAT, a novel framework for automatically optimizing heuristics in SAT solvers. AutoSAT is based on Large Language Models (LLMs) which is able to autonomously generate codes, conduct evaluation, and then utilize feedback to further optimize heuristics, thereby reducing human intervention and enhancing solver capabilities. AutoSAT operates on a plug-and-play basis, eliminating the need for extensive enterprise and model training, and fosters a Multi-Agent-based collaborative process with fault tolerance to ensure robust heuristic optimization. We implement AutoSAT on a lightweight Conflict-Driven Clause Learning (CDCL) solver EasySAT (the volume of EasySAT is about one-fiftieth of the State-of-the-Art hybrid solver Kissat) and extensive experiments on seven datasets demonstrate its superior performance. Out of the seven testing datasets, AutoSAT shows a superior performance to Kissat in two datasets and displays an overall similar performance in three datasets. Some heuristics generated by AutoSAT are even counter-intuitive but are very effective.
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) - EduSAT: A Pedagogical Tool for Theory and Applications of Boolean
Satisfiability [4.392308906793852]
EduSAT is a tool designed to support learning and understanding of SAT and Satisfiability Modulo Theories (SMT) solving.
It offers implementations of key algorithms and solver abstractions for five NP-complete problems beyond SAT and SMT.
Users can benefit from EduSAT by experimenting, analyzing, and validating their understanding of SAT and SMT solving techniques.
arXiv Detail & Related papers (2023-08-15T17:31:35Z) - 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) - W2SAT: Learning to generate SAT instances from Weighted Literal
Incidence Graphs [13.173307471333619]
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.
arXiv Detail & Related papers (2023-02-01T06:30:41Z) - 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)
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.