SAT 求解器中基数约束编码的比较
计算机科学中的逻辑
2018-11-01 v1 组合数学
摘要
基数约束在许多 SAT 问题中十分重要；先前研究就最佳编码的使用给出了相互矛盾的结论。此处比较了三种编码：Sinz 的序列计数器、Bailleux 与 Boufkhad 的基于树的方法，以及 Abío 及其合作者的基于排序的方法。对于一系列相关的组合测试用例，序列计数器方法被发现是其中最快的。所有编码都允许辅助变量对主变量的单一解存在多个解；多解的数量可能非常庞大，并可能阻碍 SAT 求解器。我们开发了这些编码的变体，其中额外子句减少了多解的数量。这些变体被发现对求解时间影响甚微，即便子句数量大约翻倍。结果凸显了众所周知的观察：子句计数及编码大小的其他度量并不是 SAT 问题难度的可靠指标。
引用
@article{arxiv.1810.12975,
title = {A comparison of encodings for cardinality constraints in a SAT solver},
author = {Ed Wynn},
journal= {arXiv preprint arXiv:1810.12975},
year = {2018}
}
备注
27 pages