將n個xor表達式轉換爲CNF？

Question

我有n個XOR表達式：

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）。你準備好了嗎？

考慮到這種解釋，你可以通過僅僅考慮例如構造CNF形式的公式來構造該公式。 （a = 0且b = 0且c = 1且d = 1）=> 0並將其轉化爲術語（a或b或非c或非d）。然後，你對所有產生0和它們的東西都做到這一點。

如果稍微更改問題，則可以獲得更易於管理的解決方案。如果試圖給出一個XOR b XOR c XOR d = 0給一個座標解算器，你可以引入新的變量來停止指數放大，如下所示：（a XOR b = y）AND（y XOR c = z）AND（z XOR d = 0）即使（XOR b = y）沒有很好地歸結，結果也不會因爲你增加變量的數量而大大惡化。