On Continuous Local BDD-Based Search for Hybrid SAT Solving

• URL: http://arxiv.org/abs/2012.07983v1
• Date: Mon, 14 Dec 2020 22:36:20 GMT
• Title: On Continuous Local BDD-Based Search for Hybrid SAT Solving
• Authors: Anastasios Kyrillidis, Moshe Y. Vardi, Zhiwei Zhang
• Abstract summary: We propose a novel algorithm for efficiently computing the gradient needed by CLS. We study the capabilities and limitations of our versatile CLS solver, GradSAT, by applying it on many benchmark instances. The experimental results indicate that GradSAT can be a useful addition to the portfolio of existing SAT and MaxSAT solvers for solving Boolean satisfiability and optimization problems.
• Score: 40.252804008544985
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We explore the potential of continuous local search (CLS) in SAT solving by proposing a novel approach for finding a solution of a hybrid system of Boolean constraints. The algorithm is based on CLS combined with belief propagation on binary decision diagrams (BDDs). Our framework accepts all Boolean constraints that admit compact BDDs, including symmetric Boolean constraints and small-coefficient pseudo-Boolean constraints as interesting families. We propose a novel algorithm for efficiently computing the gradient needed by CLS. We study the capabilities and limitations of our versatile CLS solver, GradSAT, by applying it on many benchmark instances. The experimental results indicate that GradSAT can be a useful addition to the portfolio of existing SAT and MaxSAT solvers for solving Boolean satisfiability and optimization problems.

Related papers

• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  We derive a single differentiable function capable of approximating solutions for the Maximum Satisfiability Problem (MaxSAT) We present a novel neural network architecture to model our differentiable function, and progressively solve MaxSAT using backpropagation.
  arXiv  Detail & Related papers  (2024-02-06T02:33:00Z)
• Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers [20.866863965121013]
  MaxSAT is an optimization version of the famous NP-complete Satisfiability problem (SAT) We propose a new local search algorithm called SPB-MaxSAT that provides new perspectives for clause weighting on MaxSAT local search solvers.
  arXiv  Detail & Related papers  (2024-01-19T09:59:02Z)
• 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)
• Fully Stochastic Trust-Region Sequential Quadratic Programming for Equality-Constrained Optimization Problems [62.83783246648714]
  We propose a sequential quadratic programming algorithm (TR-StoSQP) to solve nonlinear optimization problems with objectives and deterministic equality constraints. The algorithm adaptively selects the trust-region radius and, compared to the existing line-search StoSQP schemes, allows us to utilize indefinite Hessian matrices.
  arXiv  Detail & Related papers  (2022-11-29T05:52:17Z)
• 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)
• DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving [45.21499915442282]
  We propose a novel dynamic-programming approach for solving generalized MaxSAT problems with hybrid constraints. Our versatile framework admits many generalizations of CNF-MaxSAT, such as MaxSAT, Min-MaxSAT, and MinSAT with hybrid constraints. Empirical results indicate that DPMS is able to solve certain problems quickly, where other algorithms based on various techniques all fail.
  arXiv  Detail & Related papers  (2022-05-08T00:31:53Z)
• 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)
• Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
  We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length. This problem is central in Combinatorial Testing for the detection of system failures.
  arXiv  Detail & Related papers  (2021-05-26T14:00:56Z)

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.