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问题提供了实践指导。