Natural Max-SAT Encoding of Min-SAT
Natural Max-SAT Encoding of Min-SAT
复制标题
DOI：
10.1007/978-3-642-34413-8_40
复制
发表时间：
2012-01
期刊：
影响因子：
--
通讯作者：
Adrian Kügel
中科院分区：
文献类型：
--
作者：
Adrian Kügel
我们证明了存在一种将Min-SAT实例转换为Max-SAT实例的自然编码。与以前的编码不同，这种自然编码保持相同的变量，并且Min-SAT实例的最佳赋值与相应Max-SAT实例的最佳赋值相同。除此之外，编码还可以推广到带有子句权重和硬子句的Min-SAT变体。我们进行了实验，证明我们的编码实际上是相关的，因为通过将Min-2-SAT实例转换为Max-SAT并使用Max-SAT解算器可以比直接使用最好的Min-SAT解算器更快地求解它们。
We show that there exists a natural encoding which transforms Min-SAT instances into Max-SAT instances. Unlike previous encodings, this natural encoding keeps the same variables, and the optimal assignment for the Min-SAT instance is identical to the optimal assignment of the corresponding Max-SAT instance. In addition to that the encoding can be generalized to the Min-SAT variants with clause weights and hard clauses. We conducted experiments which give evidence that our encoding is practically relevant, as Min-2-SAT instances can be solved much faster by transforming them to Max-SAT and using a Max-SAT solver than by using the best Min-SAT solver directly.