FourierSAT & continuous SAT solving
Bridging discrete constraints and continuous optimization.
I develop continuous methods for solving hybrid SAT problems. FourierSAT turns Boolean constraints into multilinear polynomials so that gradient-based search can explore the solution space. This line extends to BDD-based gradient computation in GradSAT, unconstrained optimization, and differentiable constraint satisfaction.
From Boolean constraints to continuous search
SAT asks whether a Boolean assignment can satisfy a collection of constraints. My work focuses on hybrid systems that include CNF clauses, XORs, cardinality constraints, and pseudo-Boolean constraints. A continuous representation makes gradient information available while retaining the original discrete problem as the final test.
A line of methods
- FourierSAT: represent Boolean constraints as multilinear polynomials and search a continuous relaxation.
- GradSAT: use binary decision diagrams for efficient gradient computation and support for additional constraint families.
- Unconstrained optimization: reformulate the search so it can use optimizers beyond box-constrained methods.
- FourierCSP: extend differentiable techniques to constraint satisfaction.
These local-search approaches seek satisfying assignments; failure to find one does not establish unsatisfiability.