Formalizing Dangerous SAT Encodings
Formalizing Dangerous SAT Encodings
复制标题
危险 SAT 编码的形式化
DOI：
10.1007/978-3-540-72788-0_18
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
A. Urquhart
中科院分区：
文献类型：
--
作者：
Alexander Hertel;Philipp Hertel;A. Urquhart
在本文中，我们证明了两个非常相似的和自然的SAT编码之间的指数分离，从而表明研究人员在设计编码时必须小心，以免他们意外将复杂性引入所研究的问题中。该结果为经验结果提供了正式的解释，表明问题的编码可以极大地影响其实际解决性。
我们还引入了一个独立于域的框架，以通过其编码为SAT实例添加的复杂性进行推理。这包括以下观察结果：尽管某些编码可能会增加复杂性，但其他编码实际上可以通过添加子句来使问题更容易解决，否则这些条款很难在基于分辨率的SAT溶剂中得出。此类编码可用作多时间预处理，以加快SAT算法。
In this paper we prove an exponential separation between two very similar and natural SAT encodings for the same problem, thereby showing that researchers must be careful when designing encodings, lest they accidentally introduce complexity into the problem being studied. This result provides a formal explanation for empirical results showing that the encoding of a problem can dramatically affect its practical solvability.
We also introduce a domain-independent framework for reasoning about the complexity added to SAT instances by their encodings. This includes the observation that while some encodings may add complexity, other encodings can actually make problems easier to solve by adding clauses which would otherwise be difficult to derive within a Resolution-based SAT-solver. Such encodings can be used as polytime preprocessing to speed up SAT algorithms.