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

arXiv: https://arxiv.org/abs/2506.00674 · HTML: https://mlsanity.com/paper/2506.00674/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 57 references that are in the map.
- First posted on arXiv 31 May 2025.

## Builds on (most cited first, 13 of 13)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Learning to Optimize: A Primer and A Benchmark](https://mlsanity.com/paper/2103.12828/) (2021)
- [Learning to Optimize Neural Nets](https://mlsanity.com/paper/1703.00441/) (2017)
- [Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer](https://mlsanity.com/paper/1605.00723/) (2016)
- [Explainable AI via Learning to Optimize](https://mlsanity.com/paper/2204.14174/) (2022)
- [A Hamilton-Jacobi-based Proximal Operator](https://mlsanity.com/paper/2211.12997/) (2022)
- [FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints](https://mlsanity.com/paper/1912.01032/) (2019)
- [Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs](https://mlsanity.com/paper/2308.15020/) (2023)
- [Laplace Meets Moreau: Smooth Approximation to Infimal Convolutions Using Laplace's Method](https://mlsanity.com/paper/2406.02003/) (2024)
- [Global Solutions to Nonconvex Problems by Evolution of Hamilton-Jacobi PDEs](https://mlsanity.com/paper/2202.11014/) (2022)
- [On Continuous Local BDD-Based Search for Hybrid SAT Solving](https://mlsanity.com/paper/2012.07983/) (2020)
- [Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints](https://mlsanity.com/paper/2301.09833/) (2023)
- [On SAT representations of XOR constraints](https://mlsanity.com/paper/1309.3060/) (2013)

## Abstract (arXiv)

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.