优质 SAT 翻译的框架及其在 XOR 约束 CNF 表示中的应用
计算复杂性
2014-08-06 v2
摘要
我们提出了一个用于布尔约束的优质 CNF 表示的通用框架，旨在将判定问题翻译为 SAT 问题（即判定合取范式的可满足性）。我们将该框架应用于 XOR 约束系统（也称为二元域上的线性方程组或奇偶约束系统）的表示。该通用框架定义了“表示”的概念，并提供了几种方法来通过使表示中隐含的“知识”对 SAT 求解机制显式化所需的复杂度（“硬度”）来衡量表示的质量。我们获得了通用的上界和下界。应用于 XOR 约束系统时，我们证明了在非常普遍的情况下，“优质”表示存在超多项式下界。相应的上界表明了在约束数量上的固定参数易处理性。该上界背后的度量忽略了 XOR 约束较短表示所需的辅助变量。改进的上界（针对特殊情况）考虑了这些因素，在各种硬度度量下，一幅丰富的图景开始显现。
引用
@article{arxiv.1406.7398,
title = {A framework for good SAT translations, with applications to CNF representations of XOR constraints},
author = {Matthew Gwynne and Oliver Kullmann},
journal= {arXiv preprint arXiv:1406.7398},
year = {2014}
}
备注
67 pages; second version with extended discussion of literature. Continues arXiv:1309.3060