【发布时间】：2014-02-20 04:01:00
【问题描述】：
我有 n 个异或表达式：
a xor b xor c xor d...
我想翻译成cnf： cnf的答案可以在这里找到：
http://www.wolframalpha.com/input/?i=a++XOR+b++XOR+c+XOR+d+
我想写一个转换器，但是如何实现呢？
【问题讨论】：
标签： c# algorithm math logic formula
【发布时间】：2014-02-20 04:01:00
【问题描述】：
最小的 CNF 形式是一个术语列表，每个术语的计算结果为 0 时，将整个 CNF 强制为零。如果您更改 a XOR b XOR c XOR .. 的任何输入位，则您会更改输出，因此对于 xor 其区域仅对一个位组合强制为 0，并且它们的数量呈指数级增长 - 有 n 个输入有2^(n-1)。你准备好了吗？
鉴于这种解释，您可以通过例如构造 CNF 形式的公式。 (a = 0 and b = 0 and c = 1 and d = 1) => 0 并将其转换为术语 (a OR b OR NOT c OR NOT d)。然后，您对所有产生 0 的事物执行此操作，然后将它们全部组合在一起。
如果您稍微改变问题，您可以获得更易于管理的解决方案。如果试图将 a 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) 不能很好地归结起来，随着变量数量的增加，结果也不会变得更糟。
【讨论】：