我正试图解决一个SAT问题，它只包含一个热点约束。现在我使用的是Claessen在[1]和MiniSAT的4.2节中提出的one-hot编码。
我想知道是否有更好的方法来解决这样的问题，例如，与基于cnf的SAT求解器相比，一类求解器更适合这类问题。我搜索了一下，但找不到很多关于SAT和one-hot约束的信息。
[1]成功的SAT编码技术。Magnus Bjiirk. 2009年7月25日
可满足模定理解算器通常是表达数学问题的好选择，否则将最终使用单热CNF编码。一个关键的见解是，仅使用基于CNF和dpl的解算器，您将受到单元传播能够有效发现的内容的限制。在更高的抽象层次上，有一些关于数字和集合的理论，它们可以用来在有选择地将SAT求解器应用于更合适的子问题之前修剪搜索空间。这就是SMT为您提供的，以及更强的表达能力和更令人愉快的表达关系的语言。
但是，如果你被单热约束所困扰，没有相关的高级数学问题，有更有效的方法来编码单热约束，只需要线性数量的新子句来表达关系，而不是通常的二次增长。看到
Klieber和Kwon的N个对象中选择1的高效CNF编码。