Related papers: Machine Learning Methods in Solving the Boolean Satisfiability Problem

Machine Learning Methods in Solving the Boolean Satisfiability Problem

URL: http://arxiv.org/abs/2203.04755v1
Date: Wed, 2 Mar 2022 05:14:12 GMT
Title: Machine Learning Methods in Solving the Boolean Satisfiability Problem
Authors: Wenxuan Guo, Junchi Yan, Hui-Ling Zhen, Xijun Li, Mingxuan Yuan, Yaohui Jin
Abstract summary: 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.
Score: 72.21206588430645
License: http://creativecommons.org/licenses/by-nc-sa/4.0/
Abstract: This paper reviews the recent literature on solving the Boolean satisfiability problem (SAT), an archetypal NP-complete problem, with the help of machine learning techniques. Despite the great success of modern SAT solvers to solve large industrial instances, the design of handcrafted heuristics is time-consuming and empirical. Under the circumstances, the flexible and expressive machine learning methods provide a proper alternative to solve this long-standing problem. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT, as well as recent progress on combinations of existing CDCL and local search solvers with machine learning methods. Overall, solving SAT with machine learning is a promising yet challenging research topic. We conclude the limitations of current works and suggest possible future directions.

Related papers

Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
We introduce hardware accelerated algorithms for fast SAT problem generation and a geometric SAT encoding. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models.
arXiv Detail & Related papers (2024-10-18T22:25:54Z)
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)
Machine Learning Insides OptVerse AI Solver: Design Principles and Applications [74.67495900436728]
We present a comprehensive study on the integration of machine learning (ML) techniques into Huawei Cloud's OptVerse AI solver. We showcase our methods for generating complex SAT and MILP instances utilizing generative models that mirror multifaceted structures of real-world problem. We detail the incorporation of state-of-the-art parameter tuning algorithms which markedly elevate solver performance.
arXiv Detail & Related papers (2024-01-11T15:02:15Z)
G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks [7.951021955925275]
Graph neural networks (GNNs) have emerged as a promising approach for solving the Boolean Satisfiability Problem (SAT) G4SATBench is the first benchmark study that establishes a comprehensive evaluation framework for GNN-based SAT solvers. Our results provide valuable insights into the performance of GNN-based SAT solvers.
arXiv Detail & Related papers (2023-09-29T02:50:57Z)
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)
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)
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)
End-to-End Constrained Optimization Learning: A Survey [69.22203885491534]
It focuses on surveying the work on integrating solvers and optimization methods with machine learning architectures. These approaches hold the promise to develop new hybrid machine learning and optimization methods to predict fast, approximate, structural, solutions to problems and to enable logical inference.
arXiv Detail & Related papers (2021-03-30T14:19:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.