Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization

• URL: http://arxiv.org/abs/2506.00674v1
• Date: Sat, 31 May 2025 18:58:33 GMT
• Title: Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization
• Authors: Zhiwei Zhang, Samy Wu Fung, Anastasios Kyrillidis, Stanley Osher, Moshe Y. Vardi,
• Abstract summary: We propose unconstrained continuous optimization for hybrid SAT solving by penalty terms.<n>Our results highlight the potential of combining continuous optimization and machine-learning-based methods for effective hybrid SAT solving.
• Score: 25.30924681709063
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The Boolean satisfiability (SAT) problem lies at the core of many applications in combinatorial optimization, software verification, cryptography, and machine learning. While state-of-the-art solvers have demonstrated high efficiency in handling conjunctive normal form (CNF) formulas, numerous applications require non-CNF (hybrid) constraints, such as XOR, cardinality, and Not-All-Equal constraints. Recent work leverages polynomial representations to represent such hybrid constraints, but it relies on box constraints that can limit the use of powerful unconstrained optimizers. In this paper, we propose unconstrained continuous optimization formulations for hybrid SAT solving by penalty terms. We provide theoretical insights into when these penalty terms are necessary and demonstrate empirically that unconstrained optimizers (e.g., Adam) can enhance SAT solving on hybrid benchmarks. Our results highlight the potential of combining continuous optimization and machine-learning-based methods for effective hybrid SAT solving.

Related papers

• Efficient QAOA Architecture for Solving Multi-Constrained Optimization Problems [3.757262277494307]
  This paper proposes a novel combination of constraint encoding methods for the Quantum Approximate Optimization Ansatz.<n>One-hot constraints are enforced through $XY$-mixers that restrict the search space to the feasible sub-space naturally.<n>We benchmark the combined method against the established QUBO formulation, yielding a better solution quality and probability of sampling the optimal solution.
  arXiv  Detail & Related papers  (2025-06-03T17:46:53Z)
• Single-loop Algorithms for Stochastic Non-convex Optimization with Weakly-Convex Constraints [49.76332265680669]
  This paper examines a crucial subset of problems where both the objective and constraint functions are weakly convex.<n>Existing methods often face limitations, including slow convergence rates or reliance on double-loop designs.<n>We introduce a novel single-loop penalty-based algorithm to overcome these challenges.
  arXiv  Detail & Related papers  (2025-04-21T17:15:48Z)
• A Novel Unified Parametric Assumption for Nonconvex Optimization [53.943470475510196]
  Non optimization is central to machine learning, but the general framework non convexity enables weak convergence guarantees too pessimistic compared to the other hand.<n>We introduce a novel unified assumption in non convex algorithms.
  arXiv  Detail & Related papers  (2025-02-17T21:25:31Z)
• No-Regret Constrained Bayesian Optimization of Noisy and Expensive Hybrid Models using Differentiable Quantile Function Approximations [0.0]
  Constrained Upper Quantile Bound (CUQB) is a conceptually simple, deterministic approach that avoids constraint approximations. We show that CUQB significantly outperforms traditional Bayesian optimization in both constrained and unconstrained cases.
  arXiv  Detail & Related papers  (2023-05-05T19:57:36Z)
• Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints [39.96302127802424]
  We study a new application of hybrid Boolean constraints, which arises in quantum computing. The problem relates to constrained perfect matching in edge-colored graphs. We show that direct encodings of the constrained-matching problem as hybrid constraints scale poorly and special techniques are still needed.
  arXiv  Detail & Related papers  (2023-01-24T06:14:24Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  Constrained optimization problems abound in industry, from portfolio optimization to logistics. One of the major roadblocks in solving these problems is the presence of non-trivial hard constraints which limit the valid search space. In this work, we encode arbitrary integer-valued equality constraints of the form Ax=b, directly into U(1) symmetric networks (TNs) and leverage their applicability as quantum-inspired generative models.
  arXiv  Detail & Related papers  (2022-11-16T18:59:54Z)
• Learning Proximal Operators to Discover Multiple Optima [66.98045013486794]
  We present an end-to-end method to learn the proximal operator across non-family problems. We show that for weakly-ized objectives and under mild conditions, the method converges globally.
  arXiv  Detail & Related papers  (2022-01-28T05:53:28Z)
• Multi-Objective Constrained Optimization for Energy Applications via Tree Ensembles [55.23285485923913]
  Energy systems optimization problems are complex due to strongly non-linear system behavior and multiple competing objectives. In some cases, proposed optimal solutions need to obey explicit input constraints related to physical properties or safety-critical operating conditions. This paper proposes a novel data-driven strategy using tree ensembles for constrained multi-objective optimization of black-box problems.
  arXiv  Detail & Related papers  (2021-11-04T20:18:55Z)
• 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)
• On Continuous Local BDD-Based Search for Hybrid SAT Solving [40.252804008544985]
  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.
  arXiv  Detail & Related papers  (2020-12-14T22:36:20Z)
• A Hybrid Framework Using a QUBO Solver For Permutation-Based Combinatorial Optimization [5.460573052311485]
  We propose a hybrid framework to solve large-scale permutation-based problems using a high-performance quadratic unconstrained binary optimization solver. We propose techniques to overcome the challenges in using a QUBO solver that typically comes with limited numbers of bits.
  arXiv  Detail & Related papers  (2020-09-27T07:15:25Z)

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.