ACM通信
ACM通信
布尔可满足性:理论与工程
布尔可满足性问题(SAT，简称SAT)询问一个给定的布尔公式(带有AND和NOT等布尔门)是否对其输入变量赋值为0和1，从而使该公式得到值1。自斯蒂芬·库克证明SAT以来，它一直是计算机科学的核心问题NP在1971年完成。解决Pvs。NP这个问题是计算机科学和数学中最突出的开放式问题之一，人们必须表明SAT是否合格P即能否在多项式时间内求解。
同时，SAT是一个典型的约束满足问题，有许多应用，包括硬件和软件设计、运筹学、生物信息学等。当今大多数sat解题算法都是基于马丁·戴维斯和希拉里·帕特南在1958年为美国国家安全局撰写的一份技术报告中的工作。虽然我们似乎离解决SAT计算复杂度的问题还有很长的路要走，但工程方面的进展已经非常惊人了。现代SAT求解器通常会解决包含数百万个变量的工业SAT实例，并被硬件和软件设计师每天使用。
工程方面令人印象深刻的进步和理论方面非常缓慢的进步之间的差距导致了一个不同寻常的研讨会，题为“应用SAT求解的理论基础”，去年1月在加拿大班夫国际数学创新和发现研究站举行http://www.birs.ca/events/2014/5-day-workshops/14w5101)．这次研讨会汇集了顶尖的sat复杂性理论家和sat解决工程师，这两组人很少在一起见面，也很少说同一种技术语言。当时的希望是，让理论家和工程师接触SAT理论和工程的最新发展，将缩小这些群体之间的鸿沟。
当然，人们不能指望在两个不同的技术社区之间在一周内建起坚固的桥梁，但这不应减少这种桥梁建造讲习班的巨大价值。虽然可能需要数年时间才能看到这次研讨会是否会取得具体成果，但一些基本的研究挑战已经出现。
出现的最基本的挑战是计算复杂性理论的核心。该理论通常基于最坏情况复杂性分析，它关注最难解决的实例。最坏情况复杂度分析在数学上已经被证明是相当容易处理的，比平均情况复杂度分析要容易得多。从实用的角度来看，这似乎也是直观的;例如，算法的最坏情况上限在实践中提供了其运行时间的绝对上限。因此，最坏情况分析是复杂性理论的标准方法。然而，有一点已经变得清晰，而且在SAT研讨会上也变得令人痛苦地明显起来，那就是，最坏情况分析实际上对算法在现实生活实例中的行为没有多少启发。例如，理论家已经证明，目前的SAT求解算法必须花费指数级的时间来求解某些SAT实例族。实践者对这样的界限只是耸耸肩，而他们继续将他们的求解器应用到非常大但实际上可以解决的SAT实例中。理论的一个作用是为工程提供指导，但最坏情况(和平均情况)复杂性似乎对那些在理论上困难但在实践中可行的问题提供了很少的指导。 What is needed is a new computational complexity model, which will capture better the concept of "complexity in practice."
另一种性质不同的挑战适用于SAT工程师进行研究的方式。目前的SAT工程研究具有很强的启发式。研究人员设计了新的启发式方法，并在各种基准测试套件上测试其有效性。一年一度的SAT竞赛是一个强大的动力，因为赢得比赛是快速获得专业认可的途径。不可否认的是，这种研究方式为社会提供了良好的服务，导致了SAT解决方法的巨大进步，研究人员开玩笑地称其为“SAT摩尔定律”。同时，这种启发式方法缺乏科学性，不仅缺乏理论科学，而且缺乏实证科学。事实是，我们不理解为什么现代SAT求解者使用的特定启发式在实践中如此有效。此外，我们确实知道在某些问题领域，SAT求解的效率较低，但我们不知道原因。为了让SAT革命不受影响地继续下去，我们还必须关注理解，而不仅仅是基准测试。
所以这个研讨会的底线是我们需要更好的理论和更好的工程。我们的工作被安排好了!
摩西·y瓦迪主编
数字图书馆是由计算机协会出版的。版权所有©2014 ACM, Inc.
没有发现记录