并行连续局部搜索研究

# 并行连续局部搜索研究 来源：https://arxiv.org/html/2606.06656 \\hideLIPIcs 计算学院，澳大利亚国立大学，堪培拉，澳大利亚\.cody\.christopher@anu\.edu\.auhttps://orcid\.org/0000\-0001\-8444\-2292 计算学院，澳大利亚国立大学，堪培拉，澳大利亚\.charles\.gretton@anu\.edu\.auhttps://orcid\.org/0000\-0001\-9803\-0168\\CopyrightCody J Christopher 和 Charles Gretton\\ccsdesc\[500\]计算数学 组合优化\\ccsdesc\[500\]计算数学 求解器\\ccsdesc\[500\]计算数学 非凸优化\\supplement\\afsimplementation withApache\-2\.0/GPL\-2\.0\-or\-laterlicenses:\\supplementdetails\[linktext=, cite=, subcategory=源代码, swhid= \]软件https://github\.com/cjchristopher/accelerated\-fourier\-sat/\\EventEditors\\EventNoEds0\\EventLongTitle\\EventShortTitle\\EventAcronym\\EventYear\\EventDate\\EventLocation\\EventLogo\\SeriesVolume\\ArticleNo ###### 摘要 我们研究并行连续局部搜索（CLS）作为解决具有对称伪布尔（PB）约束的布尔可满足性问题的一种方法。这里，\(n\)变量PB可满足性问题被松弛为一个连续优化问题，该问题在\(n\)维超立方体上具有可微目标函数。对于可满足的实例，该优化问题的全局最小值对应于所处理SAT问题的满足赋值。我们通过实证实验提出了几个新颖发现：（i）冗余约束可能抑制而不是加速收敛；（ii）CLS在混合设置中作为子求解器显示出前景，能快速完成部分赋值；（iii）由于目标函数中密集存在鞍点，局部搜索迅速收敛到解质量的稳定分布（即满足程度），此时额外求解步骤会产生递减的回报。我们的发现为在现代加速器硬件上将CLS应用于SAT提供了实际指导。 ###### 关键词：可满足性，伪布尔，SAT求解器，连续局部搜索，组合优化，硬件加速 ## 1 引言 连续局部搜索（CLS）提供了一种本质上可并行化且适用于GPU加速的替代方案。CLS通过Walsh-Fourier展开\[odonnell14\]将布尔变量松弛为\[-1,1\]上的实数值，将可满足性问题重新表述为有界非凸连续优化。该方法在FourierSAT\[kyrillidis2021solving\]中被形式化，并在FastFourierSAT\[cen2025massively\]中扩展到GPU计算。一篇同行论文\[christopher2026afsat\]描述了我们的求解器Accelerated Fourier SAT (\\afs)的工程实现和性能，本文使用该求解器进行实证评估。我们做出以下贡献： 1. (a)我们分析了原生伪布尔（PB）编码相对于CNF转换在CLS中的表示优势（第2.4节 (https://arxiv.org/html/2606.06656#S2.SS4)）。 2. (b)我们给出了所有实际感兴趣的对称PB约束类型的傅里叶系数闭式推导（附录A (https://arxiv.org/html/2606.06656#A1)）。 3. (c)我们提供了实证案例研究，揭示了CLS行为中的新现象，包括梯度相互作用效应、部分赋值求解和收敛性分析（第3节 (https://arxiv.org/html/2606.06656#S3)）。 ## 2 背景 ### 2.1 Walsh-Fourier变换 我们回顾布尔函数的分析性质，特别是它们可以松弛为\(\mathbb{R}\)中的连续函数，其中\(\{\texttt{True},\texttt{False}\}\mapsto\{-1,1\}\)。对于布尔公式\(\phi:\{\top,\bot\}^n\mapsto\{\top,\bot\}\)，连续松弛为\(\text{Rel}_\phi:[-1,1]^n\mapsto[-1,1]\)。\([-1,1]^n\)是凸布尔超立方体\(\mathcal{Q}^n\)。Walsh-Fourier展开\[odonnell14,kyrillidis2021solving\]就是这样的松弛： \[\texttt{FE}_\phi(\mathbf{X})\stackrel{\scriptstyle\text{def}}{=}\sum_{S\in 2^{\mathbf{X}}}\hat{f}(S)\prod_{x_i\in S}x_i \quad(1)\] 其中\(\mathbf{X}\)是\(n\)个变量的集合，\(\hat{f}(S)\)是在子集\(S\subseteq\mathbf{X}\)上的*傅里叶系数*。\(\texttt{FE}_\phi\)是一个多线性多项式——由*初等对称多项式*（ESP）线性组合而成。 \[e_n=\sum_{1\le j_1<j_2<\cdots<j_m\le n}\prod_{k=1}^m x_{j_k}\] 初等对称多项式\(e_n\)跨越了所有对称布尔函数的空间。给定对称PB约束，使用本文的闭式系数，傅里叶系数计算代价是\(O(n)\)或\(O(n\log^2 n)\)。 ### 2.2 连续局部搜索 对于CNF，\(\phi\)被表示为\(\texttt{FE}_\phi\)，这是一个连续函数。CLS通过梯度下降迭代优化\(\texttt{FE}_\phi\)，以全局最小值为目标。由于\(\texttt{FE}_\phi\)在\([-1,1]^n\)上是平滑的，梯度下降是可微的且具有高度并行性。我们使用Nesterov加速梯度（NAG）更新，并配置为完全并行的启动和评估。\(\texttt{FE}_\phi\)评估需要计算所有ESP，这些ESP可以在\(O(n\log^2 n)\)时间内通过基于快速傅里叶变换（FFT）的算法计算。我们的加速器\afs实现了这种计算策略，针对GPU架构进行了优化，在下文中记为FastFourierSAT。 ### 2.3 对称伪布尔约束 对称PB约束是谓词，其真值仅取决于其变量的赋值计数。示例包括： *AtLeast-k*： \(\sum_n x_n \ge k\) *AtMost-k*： \(\sum_n x_n \le k\) *Exactly-k*： \(\sum_n x_n = k\) *Parity*： \(\sum_n x_n \equiv 1 \pmod{2}\) *Cardinality-k*： \(\sum_n x_n \ge k\)（也称为基数约束）。 表1总结了这些约束在给定傅里叶系数下的代价。 ### 2.4 原生PB与CNF编码 表1：对称PB约束的原生CLS代价与CNF转换代价的比较。原生CLS代价是指计算\(\texttt{FE}_\phi\)所需的ESPs数量；CNF转换代价是指引入的子句数和辅助变量数。注意原生PB编码避免了CNF转换中的辅助变量，从而降低了表示代价。 \begin{tabular}{|l|c|c|c|c|} \hline **约束类型** & **原生CLS代价** & **CNF子句数** & **CNF辅助变量** \\ \hline 至少-k & \(O(1)\) & \(O(1)\) & \(O(1)\) \\ \hline 至多-k & \(O(1)\) & \(O(1)\) & \(O(1)\) \\ \hline 恰好-k & \(O(1)\) & \(O(n)\) & \(O(1)\) \\ \hline 异或（XOR） & \(O(n)\) & \(O(n)\) & \(O(1)\) \\ \hline 基数-k（CARD） & \(O(n\log^2 n)\) & 见表2 & 见表2 \\ \hline \end{tabular} 表2：傅里叶系数计算与对称PB约束的CNF转换的渐近成本比较。 \begin{tabular}{|l|c|c|} \hline **编码** & **\#子句** & **\#辅助变量** \\ \hline 朴素 & \(\binom{n}{k+1}\) & 0 \\ \hline 顺序一元计数器 & \(O(n\cdot k)\) & \(O(n\cdot k)\) \\ \hline 并行二进制计数器 & \(7n-3\lfloor\log n\rfloor-6\) & \(2n-2\) \\ \hline Bailleux和Boufkhad\[bailleux2003efficient\] & \(O(n^2)\) & \(O(n\cdot\log n)\) \\ \hline Warners\[warners1998linear\] & \(8n\) & \(2n\) \\ \hline \end{tabular} 表3：基数-k的CNF编码\[sinz2005towards\]。所有非朴素编码都引入了辅助变量。