Self-Satisfied: An end-to-end framework for SAT generation and prediction

• URL: http://arxiv.org/abs/2410.14888v1
• Date: Fri, 18 Oct 2024 22:25:54 GMT
• Title: Self-Satisfied: An end-to-end framework for SAT generation and prediction
• Authors: Christopher R. Serrano, Jonathan Gallagher, Kenji Yamada, Alexei Kopylov, Michael A. Warren,
• Abstract summary: 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.
• Score: 0.7340017786387768
• License:
• Abstract: The boolean satisfiability (SAT) problem asks whether there exists an assignment of boolean values to the variables of an arbitrary boolean formula making the formula evaluate to True. It is well-known that all NP-problems can be coded as SAT problems and therefore SAT is important both practically and theoretically. From both of these perspectives, better understanding the patterns and structure implicit in SAT data is of significant value. In this paper, we describe several advances that we believe will help open the door to such understanding: we introduce hardware accelerated algorithms for fast SAT problem generation, a geometric SAT encoding that enables the use of transformer architectures typically applied to vision tasks, and a simple yet effective technique we term head slicing for reducing sequence length representation inside transformer architectures. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. We validate our architecture, termed Satisfiability Transformer (SaT), on the SAT prediction task with data from the SAT Competition (SATComp) 2022 problem sets. Prior related work either leveraged a pure machine learning approach, but could not handle SATComp-sized problems, or was hybrid in the sense of integrating a machine learning component in a standard SAT solving tool. Our pure machine learning approach achieves prediction accuracies comparable to recent work, but on problems that are an order of magnitude larger than previously demonstrated. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models. We both describe experimental results that probe the landscape of where SAT data can be successfully used for learning and position these results within the broader context of complexity and learning.

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)
• 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)
• 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)
• W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [11.139131079925113]
  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.