具有社区结构的SAT问题的困难性
计算机科学中的逻辑
2016-08-16 v4 计算复杂性
摘要
近期，为了解释基于冲突驱动子句学习（CDCL）的布尔可满足性（SAT）求解器在大型工业基准上的有效性，研究集中于社区结构这一概念。具体而言，经验发现工业基准具有良好社区结构，且实验似乎显示此种结构与CDCL效率之间存在相关性。然而，本文给出了困难性结果，表明社区结构不足以解释CDCL在实践中的成功。首先，我们正式刻画了一大类捕捉社区结构的度量（包括“模块度”）所共享的一个性质。接着，我们证明，依据具有该性质的任意度量具有良好社区结构的SAT实例仍是NP难的。最后，我们研究了一类由Giráldez-Cru与Levy的“伪工业”社区附着模型生成的随机实例。我们证明，以高概率，该模型中具有相对较少但高度模块化的社区的实例需要指数级长的归结证明，因而对CDCL是困难的。我们还给出了实验证据，表明我们的结果对具有更多社区的实例依然成立。这表明，被CDCL轻松解决的实际工业实例可能具有社区附着模型未捕捉到的其他相关结构。
引用
@article{arxiv.1602.08620,
title = {On the Hardness of SAT with Community Structure},
author = {Nathan Mull and Daniel J. Fremont and Sanjit A. Seshia},
journal= {arXiv preprint arXiv:1602.08620},
year = {2016}
}
备注
23 pages. Full version of a SAT 2016 paper