0

假设您有一个布尔函数，它接受两个数字（二进制​​）并在它们等于 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 时唯一关心的问题，还是有助于包括这些观察到的约束？

我意识到这不是一个很好的例子，但希望它能解释我的要求。

提前致谢

4

1 回答 1

1

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

这可以实现为这样的多级逻辑电路： 在此处输入图像描述

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

通常的方法是先用合取范式(CNF) 对问题进行编码，然后让 SAT 求解器找到一个解决方案或找到无法满足的问题。大多数 SAT 求解器很少能找到所有解。

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

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

于 2013-05-26T22:02:11.923 回答