迈向良好 SAT 表示的理论
人工智能
2013-05-13 v4 计算机科学中的逻辑
摘要
我们旨在为布尔函数 f 的“良好”SAT 表示 F 奠定理论基础。我们认为，由作者引入的 k 级单元反驳完备子句集层级 UC_k 提供了最基本的目标类，即应尽可能实现较小的 k 使得 F 属于 UC_k。如果 F 不包含新变量，即 F（作为 CNF）等价于 f，那么 F 属于 UC_1 类似于文献中已知的“实现（广义）弧一致性”（它稍弱一些，但在理论上更易于处理）。我们表明，在此意义上，布尔函数的多项式大小表示的 UC_k 层级是严格的。用于这些分离的布尔函数是亏格为 1 的“掺杂”极小不可满足子句集；这些函数由 [Sloan, Soerenyi, Turan, 2007] 引入，我们推广了它们的构造并展示了其与强化版的冗余子句集概念的对应关系。从下界转向上限，我们认为许多常见的 CNF 表示符合 UC_k 方案，并基于 Tseitin 翻译给出了一些在 UC_1 中构建含新变量表示的基本工具。注意，关于新变量，UC_1 表示比单纯的“弧一致性”更强，因为新变量并未被排除在考虑之外。
引用
@article{arxiv.1302.4421,
title = {Towards a theory of good SAT representations},
author = {Matthew Gwynne and Oliver Kullmann},
journal= {arXiv preprint arXiv:1302.4421},
year = {2013}
}
备注
59 pages; second version with some extended discussions and editorial corrections, third version with extended introduction, more examples and explanations, and some editorial improvements, fourth version with further examples, explanations and discussions, and with added computational experiments