satisfiability - SAT-Solving a system of one-hot 约束

Question

我正在尝试解决仅包含单热约束的 SAT 问题。现在我正在使用 Claessen 在 Sec. 中提出的 one-hot 编码。[1] 的 4.2 和 MiniSAT。

我想知道是否有解决此类问题的更好方法，例如与基于 CNF 的 SAT 求解器相比，一类求解器更适合此类问题。我搜索了一下，但根本找不到关于 SAT 和 one-hot 约束的太多信息。

[1]成功的 SAT 编码技术。马格努斯·比吉尔克。2009 年 7 月 25 日

Answer 1

可满足性模定理求解器通常是表达数学问题的好选择，否则这些问题最终会使用一次性 CNF 编码。一个关键的见解是，仅使用基于 CNF 和 DPLL 的求解器，您就受限于单元传播可以有效发现的内容。在更高的抽象层次上，在有选择地将 SAT 求解器应用于更合适的子问题之前，可以使用数字和集合的理论来修剪搜索空间。这就是 SMT 为您提供的，以及更强大的表达能力和更令人愉悦的表达关系的语言。

但是，如果您遇到没有关联的更高级别数学问题的 onehot 约束，则有更有效的方法来编码 onehot 约束，只需要线性数量的新子句来表达关系，而不是通常的二次增加。看

Klieber 和 Kwon从 N 个对象中选择 1 个的高效 CNF 编码。