constraint-programming - SAT求解器中N个编码中的至少K个

Question

我知道，给定 N 中最多 k 个工具，我可以通过将其更改为 N 中最多 (nk) 来得到 N 中的至少 K。

但我似乎无法理解这是怎么回事。我可能会遗漏一些非常微不足道的东西

例如，如果 K=2 和 N=6，如何至少 2 out of 6 等于最多 4 out of 6

任何帮助，将不胜感激

Answer 1

正如你所说，等价是不正确的。所以，不要因为不理解而感到难过。看，让我们举个例子。假设我们只有布尔值 N=6和 K=2以及赋值：

True False False False False False

对这 6 个变量。At most 2 out of 6 are True这个赋值显然满足了该语句，但事实并非At least 4 out of 6 are True如此。

也许你的意思是：

N 个中至少有 K 个为真

相当于

N 中最多 NK 为 False

可以进一步概括为：

N 个对象中至少有 K 个具有属性 P

相当于：

N 个对象中最多 NK 个不具有属性 P

这就是你想要表达的吗？希望这更清楚！