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

Question

我知道，给定 N 中最多 k 个工具，我可以通过将其更改为 N 中最多 (n-k) 个工具，从 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 中最多 N-K 为假

可以进一步概括为：

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

相当于：

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

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