performance - 如何实现超级优化器

Question

我对如何编写超级优化器很感兴趣。特别是要找到位和的小逻辑公式。这以前被设置为对 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。

事实证明，至少在理论上，当 x =1 时，有一种巧妙的方法可以解决这个问题。但是，我正在寻找一种计算密集型方法来搜索小型解决方案。

How can you make a superoptimizer for this problem?

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

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

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

score 2 · Accepted Answer

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

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

score 1 · Accepted Answer

如果我理解您的要求，您将需要研究逻辑最小化和/或布尔函数简化的一般主题。这些参考文献主要是关于消除布尔公式中冗余的一般方法，这些布尔公式是作为连词（“和”）的术语的析取（“或”）。

手工，标准方法称为卡诺图。以更适合计算机实现的方式表达的等效算法是 Quine-McKlosky（也称为质蕴涵法）。最小化问题是 NP 难的，而 QM 正好解决了它。

因此，我认为 QM 是您想要构建的“超级优化器”所需要的。

但是 NP-hard 和精确解的结合意味着 QM 对于大问题是不切实际的，至少是不平凡的问题。

QM 算法在表格中列出连接词（在此上下文中称为最小词），并搜索词对之间的 1 位差异。这些术语可以组合在一起，并且在进一步组合中标记为“不关心”的不同位的因素。这以 2 位、4 位等位子集重复。指数行为的结果是因为涉及到更大位集的组合的选择：选择一个排除另一个。因此，它本质上是一个搜索问题。

有大量关于启发式的文献来修剪搜索空间，但找到不一定是最优的“好”解决方案。一个著名的是浓缩咖啡。然而，由于算法改进直接转化为半导体制造的收入，因此最好的完全有可能是专有的并且被密切持有。

2 回答 2