近日，计算机系长聘教轨副教授Dominik Scheder在理论计算机领域中最重要的NP完全问题k-SAT问题上的研究取得了重大进展——得到了目前为止最好的NP完全问题求解时间复杂度界。相关成果“PPSZ is better than you think”已被理论计算机界的顶级会议IEEE Symposium on Foundations of Computer Science（FOCS）2021接收。Dominik Scheder为论文的唯一作者。

该论文首次指出了1998年对PPSZ算法的分析是次优的，且在未对算法本身做任何修改的前提下给出了一个更加完全的算法复杂度分析。该论文为后续研究PPSZ算法真实时间复杂度分析奠定了基础。

本研究由国家自然科学基金下的项目“布尔可满足性算法和单调布尔函数的复杂性”提供支持。

研究背景

布尔可满足性问题（SAT）是NP问题中的重要成员，是一类重要的确定性优化问题。

图1: 3-CNF公式（SAT问题举例）

论文题目"PPSZ is better than you think"中提到的PPSZ算法是用于求解SAT问题的经典算法，由Paturi, Pudlak, Saks 和 Zane在1998年提出。PPSZ算法的核心思想是通过对解的编码的求解来对实现SAT问题的求解。具体的执行过程如下：首先，给定一组布尔变量，并对进行随机重排列，记为。其中，对于可以根据特殊规则确定的，无需考虑它们的取值选取。随机选取t个比特对剩余的t个进行随机赋值，将赋值后的作为概率性SAT算法的输入，输出的t个随机比特恰好对应解的概率为，这里的t个随机比特也称为解的编码比特。

作者Paturi, Pudlak, Saks 和 Zane给出的对PPSZ算法的原始的复杂度分析方法是，通过判断解的编码比特的长度，得到PPSZ算法的复杂度。而Hansen, Kaplan, Zamir和 Zwick在STOC 2019上发表的论文中提到，可以通过将PPSZ算法的输入修改有倾向性随机比特，提高PPSZ算法的求解效率。

创新成果

本论文改进了PPSZ算法的复杂度分析方法，得到了一个更优的时间复杂度界。作者优化该复杂度分析方法的主要优化思路是：

1. 按一种特定的分布对布尔变量进行赋值，而非直接均匀随机地对其赋值。此时，我们可以得到一个更短的编码；

2. 不需要真实对进行采样赋值，只需模拟描绘的赋值随机性即可。

具体的分析过程类似于对树的路径灭绝问题的分析：

图2：二叉树的路径灭绝：左边的树有可以避开所有红色节点走到叶子节点的路径；右边的树不存在这种路径，称之为二叉树的路径灭绝

FOCS由IEEE计算机学会的计算机数学基础专委会提供资助，是计算机科学领域最顶级的国际会议，并被公认属于难度最高的会议之一，与ACM计算理论年会（STOC）并称理论计算机科学两大顶会。FOCS会议涵盖的领域十分广泛，包括算法和数据结构、计算复杂性、密码学、计算几何、算法图论与组合学、计算随机性、计算博弈论和量子计算等。

FOCS的前身为1960年成立的开关电路理论与逻辑设计研讨会（Symposium on Switching Circuit Theory and Logical Design），在1966年举行的第7次会议时，名称改为开关和自动机理论研讨会（Symposium on Switching and Automata Theory, SWAT），1975年更名为IEEE计算机科学基础研讨会（IEEE Symposium on Foundations of Computer Science，FOCS）。

作者介绍

Dominik Scheder，计算机科学与工程系长聘教轨副教授，2011年获瑞士苏黎世理工学院博士学位。曾先后在丹麦奥尔胡斯大学，加州大学伯克利分校西蒙研究所，清华大学任博士后研究学者。2014年加入上海交大计算机系工作。

文稿丨Dominik Scheder、夏雯雯、杜晓东、张杰琳