A Study of Parallel Continuous Local Search
For SAT practitioners using continuous optimization, this provides empirical insights into the behavior of CLS, though findings are incremental.
The paper studies parallel Continuous Local Search (CLS) for Boolean satisfiability with pseudo-Boolean constraints, finding that redundant constraints inhibit convergence, CLS works well as a sub-solver for partial assignments, and local search quickly reaches a stable solution quality due to saddle-dense objectives.
We study parallel Continuous Local Search (CLS) as a solution approach for Boolean satisfiability problems with symmetric pseudo-Boolean (PB) constraints. Here, the $n$-variable PB-satisfiability problem is relaxed to a continuous optimisation problem with a differentiable objective function on an $n$-dimensional hypercube. For satisfiable instances, the global minimisers of this optimisation problem correspond to satisfying assignments of the SAT problem at hand. We present several novel findings via empirical experiments: (i) redundant constraints can inhibit rather than accelerate convergence; (ii) CLS shows promise as a sub-solver in hybridised settings, quickly completing partial assignments; and (iii) local search rapidly converges to a stable distribution of solution quality (i.e., degree of satisfaction), due to saddle-dense objectives where additional solver steps yield diminishing returns. Our findings inform practical uses of CLS for SAT on modern accelerator hardware.