  The Boolean SATisfiability problem (SAT) is of central importance in computer
science. Although SAT is known to be NP-complete, 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, SAT solvers that are effective on other types of
constraints, e.g., cardinality constraints and XORs, are less well studied; a
general approach to handling non-CNF constraints is still lacking. In addition,
previous work indicated that for specific classes of benchmarks, the running
time of extant SAT solvers depends heavily on properties of the formula and
details of encoding, instead of the scale of the benchmarks, which adds
uncertainty to expectations of running time.
  To address the issues above, we design FourierSAT, an incomplete SAT solver
based on Fourier analysis of Boolean functions, a technique to represent
Boolean functions by multilinear polynomials. By such a reduction to continuous
optimization, we propose an algebraic framework for solving systems consisting
of different types of constraints. The idea is to leverage gradient information
to guide the search process in the direction of local improvements. Empirical
results demonstrate that FourierSAT is more robust than other solvers on
certain classes of benchmarks.
