c# - 将 n xor 表达式翻译成 CNF？

Question

我有 n 个异或表达式:

a xor b xor c xor d...

我想翻译成cnf:cnf的答案可以在这里找到:

http://www.wolframalpha.com/input/?i=a++XOR+b++XOR+c+XOR+d+

我想写一个转换器，但我该如何实现呢？

Answer 1

最小的 CNF 形式是一个项列表，当每个项的计算结果为 0 时，强制整个 CNF 为零。如果你改变 XOR b XOR c XOR 的任何输入位 .. 你改变了输出，所以对于 xor 它的区域所有强制 0 仅用于一个位组合，并且它们的数量呈指数级增长 - n 输入有2^(n-1)。你准备好了吗？

鉴于这种解释，您只需采用例如(a = 0 and b = 0 and c = 1 and d = 1) => 0 并将其转化为项 (a OR b OR NOT c OR NOT d)。然后，您对产生 0 的所有内容执行此操作，并将它们全部放在一起。

如果稍微更改问题，您可以获得更易于管理的解决方案。如果我们试图将 XOR b XOR c XOR d = 0 提供给 sat 求解器，您可以引入新变量来停止指数爆炸，如下所示:(a XOR b = y) AND (y XOR c = z) AND (z XOR d = 0) 即使 (a XOR b = y) 不能很好地归结，结果也不会随着变量数量的增加而变得更糟。