performance - 如何实现 super 优化器

Question

[与https://codegolf.stackexchange.com/questions/12664/implement-superoptimizer-for-addition相关从 2013 年 9 月 27 日开始]

我感兴趣的是如何写superoptimizers .特别是要找到位和的小逻辑公式。之前将其设置为 codegolf 的挑战，但它似乎比人们想象的要难得多。

我想编写代码来找到最小可能的命题逻辑公式，以检查 y 个二进制 0/1 变量的总和是否等于某个值 x。让我们称变量为 x1、x2、x3、x4 等。在最简单的方法中，逻辑公式应该等于总和。也就是说，当且仅当总和等于 x 时，逻辑公式才为真。

这是一个简单的方法。假设 y=15 和 x = 5。选择所有 3003 种不同的方式来选择 5 个变量，并为每个创建一个新的子句，其中包含这些变量的 AND 以及其余变量的否定的 AND。您最终得到 3003 个子句，每个子句的长度恰好为 15，总成本为 45054。

但是，如果您被允许在您的解决方案中引入新变量，那么您可以通过消除常见的子公式来大大减少这种情况。所以在这种情况下，您的逻辑公式由 y 个二进制变量、x 和一些新变量组成。当且仅当 y 变量的总和等于 x 时，整个公式才可满足。唯一允许的运算符是 and、or 和 not。

原来有一个clever method当 x = 1 时解决这个问题，至少在理论上是这样。但是，我正在寻找一种计算密集型方法来搜索小的解决方案。

How can you make a superoptimizer for this problem?

例子。以两个变量为例，我们需要一个逻辑公式，当它们的总和为 1 时恰好为真。一个可能的答案是:

(((not y0) and (y1)) or ((y0) and (not y1)))

要在公式中引入一个新变量，例如 z0 来表示 y0 而不是 y1，那么我们可以引入一个新的子句 (y0 and not y1) or not z0 并在整个公式的其余部分用 z0 替换 y0 and not y1 。当然，这在本示例中毫无意义，因为它会使表达式变长。

Answer 1

用二进制写下你想要的总和。首先查看最不重要的位 y0 。清楚地， x1 xor x2 xor ... xor xn = y0 - 这是你的第一个公式。最终公式将是所需总和的每一位的公式的结合。

现在，你知道加法器是如何实现的了吗？ http://en.wikipedia.org/wiki/Adder_(electronics) .从中汲取灵感，将您的输入分组为位对/三元组，计算进位位，并使用它们为 y1...yk 制作公式。如果您需要进一步的提示，请告诉我。