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.

翻译：本文研究将平行连续局部搜索（CLS）作为求解对称伪布尔（PB）约束布尔可满足性问题的方法。在此，我们将$n$变量PB-可满足性问题松弛为定义在$n$维超立方体上的可微目标函数连续优化问题。对于可满足实例，该优化问题的全局最小值点对应待求解SAT问题的满足性赋值。通过实证实验，我们提出若干新发现：（i）冗余约束会抑制而非加速收敛；（ii）CLS在混合设置中作为子求解器具有潜力，能快速完成部分赋值；（iii）由于目标函数存在鞍点密集特性（此时增加求解器步骤的收益递减），局部搜索会快速收敛到解质量（即满足程度）的稳定分布。这些发现为在现代加速硬件上应用CLS求解SAT问题提供了实践指导。