# On Continuous Local BDD-Based Search for Hybrid SAT Solving

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Dec 2020.

## Built on by (most cited first, 5 of 5)

- [Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs](https://mlsanity.com/paper/2308.15020/) (2023)
- [DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving](https://mlsanity.com/paper/2205.03747/) (2022)
- [Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints](https://mlsanity.com/paper/2301.09833/) (2023)
- [Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization](https://mlsanity.com/paper/2506.00674/) (2025)
- [FourierCSP: Differentiable Constraint Satisfaction Problem Solving by Walsh-Fourier Expansion](https://mlsanity.com/paper/2510.04480/) (2025)

## Abstract (arXiv)

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.