Solving Hybrid Boolean SAT by Continuous Optimization

The Boolean SATisfiability problem (SAT) is of central importance in computer science. Despite the NP-completeness of SAT, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, other types of non-CNF, i.e., hybrid constraints (e.g., cardinality/pseudo-Boolean constraints and XOR}s play important roles in critical applications such as cryptography, task scheduling, and quantum computing. Nevertheless, SAT solvers that are effective on hybrid constraints are less well studied; a general approach for handling hybrid constraints is still lacking. The thesis focuses on the applications and approaches for hybrid SAT solving. It starts with a motivating application of hybrid SAT solving in quantum computing. A smart hybrid SAT encoding is proposed to solve the problem with quantum interest. Then the thesis introduces efforts for addressing critical limitations of a continuous-optimization-based framework for hybrid SAT solving, named FourierSAT. In FourierSAT, Boolean constraints are converted into polynomials via Walsh-Hadamard-Fourier Transform and constrained continuous optimizers are then applied to search for a solution. FourierSAT suffers from slow gradient computation, incapability of handling pseudo-Boolean (PB) constraints, and the restriction to constrained optimizers, which together limit its potential. The thesis presents to use binary decision diagrams (BDDs) to replace polynomials, which significantly accelerates the gradient computation both in theory and practice, meanwhile handling PB constraints. The thesis then proposes an approach for removing the requirement of supporting constraints from the optimizers while still maintaining soundness, making FourierSAT compatible to several machine-learning-inspired optimizers. Empirical results demonstrate that the improved FourierSAT achieves promising performance on certain classes of applications and qualifies to be a useful complement to the SAT solver portfolio. This thesis further opens a solid research direction by bridging analysis of Boolean functions, continuous optimization and SAT solving. FourierSAT will continue benefiting from future advancements in multiple fields.

Name thesis:degree_name

Doctor of Philosophy

Level thesis:degree_level

Doctoral

Discipline thesis:degree_discipline

Engineering

Grantor

Rice University

Year dc:date.issued

2025

Author dc:creator

• Zhang, Zhiwei

Advisor dc:contributor.advisor

• Vardi, Moshe Y.

• SAT Solving
• Continuous Optimization

Statement dc:rights

• Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder.

Language dc:language.iso

eng

Handle dc:identifier.uri

https://hdl.handle.net/1911/118674

OAI identifier oai:identifier

oai:repository.rice.edu:1911/118674