布尔可满足性： 理论与工程  

By Moshe Y. Vardi 

Communications of the ACM, March 2014, Vol. 57 No. 3, Page 5

一，译文

布尔可满足性问题（Boolean Satisfiability Problem，简称 SAT）问的是，一个给定的布尔公式在 AND 和 NOT 等布尔门的作用下，其输入变量的 0 和 1 的赋值是否能使公式产生值 1。自斯蒂芬-库克（Stephen Cook）于 1971 年证明了 SAT 的 NP 完备性以来，SAT 一直是计算机科学领域的核心难题。要解决 P 与 NP 的问题--计算机科学和数学领域最悬而未决的问题之一，我们必须证明 SAT 是否在 P 中，也就是说，它是否能在多项式时间内求解。

与此同时，SAT 是一个典型的约束满足问题，应用广泛，包括硬件和软件设计、运筹学、生物信息学等。现代 SAT 求解算法大多基于马丁-戴维斯（Martin Davis）和希拉里-普特南（Hilary Putnam）1958 年为美国国家安全局撰写的技术报告。虽然我们似乎离解决 SAT 计算复杂性的问题还很遥远，但工程方面的进展却非常惊人。现代 SAT 求解器可以例行求解包含数百万个变量的工业 SAT 实例，硬件和软件设计师每天都在使用这些求解器。

工程方面的进展令人印象深刻，而理论方面的进展却非常缓慢，这种差距促成了一场不同寻常的研讨会，题为 "应用 SAT 求解的理论基础"，于今年 1 月在加拿大班夫国际数学创新与发现研究站举行（见 http://www.birs.ca/events/2014/5-day-workshops/14w5101）。研讨会汇集了顶尖的 SAT 复杂性理论家和 SAT 解题工程师，这两个群体很少在一起会面，几乎不使用同一种技术语言。他们希望让理论家和工程师了解 SAT 理论和工程方面的最新发展，从而缩小这两个群体之间的差距。

当然，我们不能指望在一周内就能在两个截然不同的技术社区之间架起稳固的桥梁，但这不应削弱此类架桥研讨会的巨大价值。虽然本次研讨会能否结出具体硕果尚需时日，但一些基本的研究挑战已经显现。

新出现的最根本挑战涉及计算复杂性理论的核心。该理论通常基于最坏情况复杂性分析，重点关注最难解决的实例。事实证明，最坏情况复杂性分析在数学上相当容易，比平均情况复杂性分析要容易得多。从实用的角度来看，它也显得很直观；例如，算法的最坏情况上限提供了实际运行时间的绝对上限。因此，最坏情况分析是复杂性理论的标准方法。然而，最坏情况分析对算法在现实生活实例中的行为几乎没有任何启示，这一点在 SAT 研讨会上也变得非常明显。例如，理论家们已经证明，当前的 SAT 求解算法必须花费指数级的时间才能求解某些 SAT 实例系列。实践者只是对这种界限耸耸肩，而继续将他们的求解器应用于非常大但实际上可以求解的 SAT 实例。理论的作用之一是为工程提供指导，但最坏情况（和平均情况）复杂度似乎无法为理论上困难但实际可行的问题提供指导。我们需要的是一种新的计算复杂性模型，它能更好地捕捉 "实践中的复杂性 « 这一概念。

不同性质的挑战适用于 SAT 工程师开展研究的方式。目前的 SAT 工程研究主要采用启发式方法。研究人员设计新的启发式方法，并在各种基准套件上测试其有效性。一年一度的 SAT 竞赛是一种强大的激励机制，因为在竞赛中获胜是快速获得专业认可的途径。不可否认的是，这种研究方式在业界起到了很好的作用，在 SAT 解题方面取得了巨大进步，研究人员戏称其为 "SAT 的摩尔定律"。与此同时，这种启发式方法缺乏科学性，不仅缺乏理论科学，也缺乏经验科学。现实情况是，我们并不了解现代 SAT 求解器采用的特定启发式方法为何在实践中如此有效。此外，我们确实知道有些问题领域的 SAT 求解器效果较差，但我们不知道原因何在。要想让 SAT 革命有增无减，我们还必须注重理解，而不仅仅是基准测试。

因此，研讨会的底线是，我们需要更好的理论和更好的工程。我们的工作任重而道远！

二，原文 （https://cacm.acm.org/magazines/2014/3/172516-boolean-satisfiability/fulltext?mobile=false#comments）

Boolean Satisfiability: Theory and Engineering

The Boolean Satisfiability Problem (SAT, for short) asks whether a given Boolean formula, with Boolean gates such as AND and NOT, has some assignment of 0s and 1s to its input variables such that the formula yields the value 1. SAT has been a problem of central importance in computer science since Stephen Cook proved its NP-completeness in 1971. To resolve the P vs. NP question, one of the most outstanding open questions in computer science and mathematics, one would have to show whether SAT is or is not in P, that is, whether it can be or cannot be solved in polynomial time.

At the same time, SAT is a paradigmatic constraint-satisfaction problem with numerous applications, including hardware and software design, operations research, bioinformatics, and more. Most modern-day SAT-solving algorithms are based on the work of Martin Davis and Hilary Putnam in a 1958 technical report written for the National Security Agency. While we still seem to be quite far from resolving the questions about the computational complexity of SAT, progress on the engineering side has been nothing short of spectacular. Modern SAT solvers routinely solve industrial SAT instances with millions of variables, and are being used by hardware and software designers on a daily basis.

The gap between the impressive progress on the engineering side and very slow progress on the theory side led to an unusual workshop, titled "Theoretical Foundations of Applied SAT Solving," held last January at the Canadian Banff International Research Station for Mathematical Innovation and Discovery (see http://www.birs.ca/events/2014/5-day-workshops/14w5101). The workshop brought together leading SAT-complexity theorists and SAT-solving engineers, two groups that rarely meet together and barely speak the same technical language. The hope was that exposing theoreticians and engineers to state-of-the-art developments in SAT theory and engineering would narrow the chasm between these communities.

Of course, one cannot expect robust bridges between two distinct technical communities to be erected in one week, but that should not diminish the tremendous value of such bridge-building workshops. While it may take years to see if this workshop will bear concrete fruits, some fundamental research challenges already emerged.

The most fundamental challenge to emerge goes to the very heart of computational complexity theory. This theory is based typically on worst-case complexity analysis, which focuses on instances that are the most difficult to solve. Worst-case complexity analysis has proven to be quite tractable mathematically, much more, than say average-case complexity analysis. It also seems intuitive from a practical point of view; for example, a worst-case upper bound for an algorithm offers an absolute upper bound on its running time in practice. Thus, worst-case analysis is the standard approach in complexity theory. What has become clear, however, and also became painfully evident at the SAT workshop, is that worst-case analysis actually sheds very little light on the behavior of algorithms on real-life instances. For example, theorists have demonstrated that current SAT-solving algorithms must take exponential time to solve certain families of SAT instances. Practitioners simply shrug at such bounds, while they continue to apply their solvers to very large but practically solvable SAT instances. One role of theory is to provide guidance to engineering, but worst-case (and average-case) complexity seems to offer little guidance for problems that are difficult in theory but feasible in practice. What is needed is a new computational complexity model, which will capture better the concept of "complexity in practice. »

A challenge of a different nature applied to the manner in which SAT engineers conduct their research. Current SAT engineering research is intensely heuristic. Researchers devise new heuristics and test their effectiveness on various benchmark suites. An annual SAT competition serves as a powerful motivator, as winning a track of the competition is a path to quick professional recognition. It is impossible to deny this style of research has served the community well, leading to such dramatic progress in SAT solving that researchers refer, jokingly, to "Moore's Law for SAT." At the same time, this heuristic approach lacks science, not only theoretical science but also empirical science. The reality is we have no understanding of why the specific sets of heuristics employed by modern SAT solvers are so effective in practice. Furthermore, we do know there are problem areas where SAT solvers are less effective, but we have no idea why. For the SAT revolution to continue unabated, we must focus also on understanding, not only on benchmarking.

So the bottom line of the workshop is that we need better theory and better engineering. Our work is cut out for us!