在计算布尔可满足性时包含隐式约束是否有益？答案

【问题标题】：Is it beneficial to include implicit constraints when computing boolean satisfiability?在计算布尔可满足性时包含隐式约束是否有益？
【发布时间】：2013-05-26 21:05:20
【问题描述】：

假设您有一个布尔函数，它接受两个数字（二进制）并在它们等于 16 时返回 true：

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


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

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

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

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

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

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

你可以像这样包含这个约束：

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

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

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

这些布尔函数在正确性上是等价的，但在门逻辑中，后者（可能）会更有效。简化为 SAT 时，建模问题是唯一需要考虑的问题，还是有助于包括这些观察到的约束？

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

提前致谢

【问题讨论】：

我有点困惑；我不太明白你在问什么，我不确定这是否是在问关于 SAT 问题的问题？

标签： algorithm complexity-theory boolean-logic computation-theory

【解决方案1】：

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

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

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

通常的方法是先在Conjunctive Normal Form (CNF) 中编码一个问题，然后让 SAT 求解器找到一个解决方案或找到无法满足的问题。大多数 SAT 求解器很难找到所有个解。

如果您有问题的布尔表达式，您首先必须将此公式转换为 CNF 或求解器能够处理的格式。合适的工具包括bc2cnf。像Z3 这样的更通用的求解器支持SMT 2.0 和除CNF 之外的其他格式（又名DIMACS）。

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

【讨论】：