algorithm - 在计算 bool 可满足性时包含隐式约束是否有益？

Question

假设您有一个 bool 函数，它接受两个数字(二进制​​)并在它们等于 16 时返回 true:

01000 + 01000 = 10000
  8   +   8   =  16    -> true


00110 + 01000 = 01110
  6   +   8   =  14    -> false

在这个例子中，函数有十个输入，我们称它们为 abcde + fghij。

在底层，它直接以门逻辑为模型并使用两个加法器和一些异或门来检查二进制字符串 10000 是否等价。

然后，我们将这个二元函数输入到 bool 可满足性算法中，以找到一组产生真实输出的输入(例如，上面的第一个示例)。

我的问题是:如果我们要明确观察到的约束，SAT 算法是否会更快地找到解决方案？

“观察到的约束”是什么意思？好吧，一个观察到的约束可能是“如果任一数字大于 16，则不必费心执行加法并返回 false”。

您可以像这样包含此约束:

(a ^ ¬b ^ ¬c ^ ¬d ^ ¬e) ^ (f ^ ¬g ^ ¬h ^ ¬i ^ ¬j) ^(你之前的函数)

另一个约束可能是“如果一个数字是偶数，另一个是奇数，则返回 false”。

((e ^ ¬j) v (¬e ^ j)) ^(你之前的函数)

这些 bool 函数在正确性上是等价的，但在门逻辑中，后者(可能)更有效。对问题建模是简化为 SAT 时唯一关心的问题，还是包含这些观察到的约束有帮助？

我知道这不是一个很好的例子，但希望它能解释我的问题。

提前致谢

Answer 1

您的示例函数在 2^10 = 1,024 种可能的输入组合中有 17 种结果为真。

这可以实现为这样的多级逻辑电路:

主区SAT solvers是无法枚举所有输入组合的问题。 10 个输入是一个相当适中的大小。 SAT 求解器通常必须处理数百、数千甚至数百万个输入变量。在 PC 上评估几个 100.000 个输入组合(约 20 个输入)非常容易。但如果超过数十亿种组合，即使不是不可能，它也会变得不切实际。

通常的做法是先把一个问题编码在Conjunctive Normal Form中(CNF)，然后让 SAT 求解器找到一个解决方案或找到无法满足的问题。对于大多数 SAT 求解器来说，找到所有 解决方案并不常见。

如果您的问题有 bool 表达式，您首先必须将此公式转换为 CNF 或求解器能够处理的格式。合适的工具包括 bc2cnf .更通用的求解器，如 Z3支持SMT 2.0和 CNF 以外的其他格式(又名 DIMACS )。

除了枚举真值表或询问像 Cryptominisat 2 这样的 SAT 求解器，您可以使用约束驱动求解器。要询问 Google 的其他条款包括“Answer set programming”。