[SAT] Deducing CNF for multi-input XOR function

From Wikipedia I knew a CNF formula for 2-input XOR: \( (\overline{A} \vee \overline{B} \vee C) \wedge (A \vee B \vee C) \wedge (A \vee \overline{B} \vee \overline{C}) \wedge (\overline{A} \vee B \vee \overline{C}) \)

I wanted to generalize it to multi-input XOR. Let's first try to use Wolfram Mathematica's CNF generator. What it will say for 2/3/4/5-input XOR functions?

In[65]:= tbl2=BooleanTable[{a,b,output}->Xor[a,b]==output,{a,b,output}];
In[66]:= BooleanConvert[BooleanFunction[tbl2,{a,b,output}],"CNF"]
Out[66]= 
(! a || ! b || ! output) &&
(! a ||   b ||   output) &&
(  a || ! b ||   output) &&
(  a ||   b || ! output)

In[67]:= tbl3=BooleanTable[{a,b,c,output}->Xor[a,b,c]==output,{a,b,c,output}];
In[68]:= BooleanConvert[BooleanFunction[tbl3,{a,b,c,output}],"CNF"]
Out[68]= 
(! a || ! b || ! c ||   output) &&
(! a || ! b ||   c || ! output) &&
(! a ||   b || ! c || ! output) &&
(! a ||   b ||   c ||   output) &&
(  a || ! b || ! c || ! output) &&
(  a || ! b ||   c ||   output) &&
(  a ||   b || ! c ||   output) &&
(  a ||   b ||   c || ! output)

In[69]:= tbl4=BooleanTable[{a,b,c,d,output}->Xor[a,b,c,d]==output,{a,b,c,d,output}];
In[71]:= BooleanConvert[BooleanFunction[tbl4,{a,b,c,d,output}],"CNF"]
Out[71]= 
(! a || ! b || ! c || ! d || ! output) &&
(! a || ! b || ! c ||   d ||   output) &&
(! a || ! b ||   c || ! d ||   output) &&
(! a || ! b ||   c ||   d || ! output) &&
(! a ||   b || ! c || ! d ||   output) &&
(! a ||   b || ! c ||   d || ! output) &&
(! a ||   b ||   c || ! d || ! output) &&
(! a ||   b ||   c ||   d ||   output) &&
(  a || ! b || ! c || ! d ||   output) &&
(  a || ! b || ! c ||   d || ! output) &&
(  a || ! b ||   c || ! d || ! output) &&
(  a || ! b ||   c ||   d ||   output) &&
(  a ||   b || ! c || ! d || ! output) &&
(  a ||   b || ! c ||   d ||   output) &&
(  a ||   b ||   c || ! d ||   output) &&
(  a ||   b ||   c ||   d || ! output)

In[72]:= tbl5=BooleanTable[{a,b,c,d,e,output}->Xor[a,b,c,d,e]==output,{a,b,c,d,e,output}];
In[73]:= BooleanConvert[BooleanFunction[tbl5,{a,b,c,d,e,output}],"CNF"]
Out[73]= 
(! a || ! b || ! c || ! d || ! e ||   output) &&
(! a || ! b || ! c || ! d ||   e || ! output) &&
(! a || ! b || ! c ||   d || ! e || ! output) &&
(! a || ! b || ! c ||   d ||   e ||   output) &&
(! a || ! b ||   c || ! d || ! e || ! output) &&
(! a || ! b ||   c || ! d ||   e ||   output) &&
(! a || ! b ||   c ||   d || ! e ||   output) &&
(! a || ! b ||   c ||   d ||   e || ! output) &&
(! a ||   b || ! c || ! d || ! e || ! output) &&
(! a ||   b || ! c || ! d ||   e ||   output) &&
(! a ||   b || ! c ||   d || ! e ||   output) &&
(! a ||   b || ! c ||   d ||   e || ! output) &&
(! a ||   b ||   c || ! d || ! e ||   output) &&
(! a ||   b ||   c || ! d ||   e || ! output) &&
(! a ||   b ||   c ||   d || ! e || ! output) &&
(! a ||   b ||   c ||   d ||   e ||   output) &&
(  a || ! b || ! c || ! d || ! e || ! output) &&
(  a || ! b || ! c || ! d ||   e ||   output) &&
(  a || ! b || ! c ||   d || ! e ||   output) &&
(  a || ! b || ! c ||   d ||   e || ! output) &&
(  a || ! b ||   c || ! d || ! e ||   output) &&
(  a || ! b ||   c || ! d ||   e || ! output) &&
(  a || ! b ||   c ||   d || ! e || ! output) &&
(  a || ! b ||   c ||   d ||   e ||   output) &&
(  a ||   b || ! c || ! d || ! e ||   output) &&
(  a ||   b || ! c || ! d ||   e || ! output) &&
(  a ||   b || ! c ||   d || ! e || ! output) &&
(  a ||   b || ! c ||   d ||   e ||   output) &&
(  a ||   b ||   c || ! d || ! e || ! output) &&
(  a ||   b ||   c || ! d ||   e ||   output) &&
(  a ||   b ||   c ||   d || ! e ||   output) &&
(  a ||   b ||   c ||   d ||   e || ! output)

Clearly, there are patterns here. "Mathematics is the study of patterns.", as they say. Can I reverse engineer Wolfram Mathematica's output?

See the last one, CNF for 5-input XOR. a/b/c/d/e are came in order, but 'output' isn't. 'output' alternating between 4-bit series like "! !" and " !! ".

My first idea was that output=~(a^b^c^d^e). This it true for 5-input XOR and 3-input XOR. But not true for 2-input XOR, 4-input XOR, etc, correct would be (a^b^c^d) without NOT. See the Jupyter notebook.

So my hypothesis was: ~(inputs XORed) for XOR function with odd number of inputs and (inputs XORed) (without NOT) for even number of inputs. This was proved by my test. The final function is:

    # to be used only for small number of inputs (less that ~12)
    def XOR_list(self, inputs:List[int]) -> int:

...

        # see the book for explanation of this slightly esoteric function
        for row in range(2**inputs_t):
            #print ("XOR_list, row", row)
            cls=[]
            tmp=[]
            for col in range(inputs_t):
                if (row>>col)&1==0:
                    cls.append(self.neg(inputs[col]))
                    tmp.append(False)
                else:
                    cls.append(inputs[col])
                    tmp.append(True)

            tmp2=functools.reduce (operator.xor, tmp)
            if (inputs_t&1)==0:
                tmp2=not(tmp2)

            if tmp2==False:
                cls.append(out)
            else:
                cls.append(self.neg(out))

            self.add_clause(cls)

...

        return out

( src )

I needed multi-input XOR for the program that can factorize GF(2)/CRC polynomials. Failed. CNF grows exponentially even for small XOR functions. It's still wiser to construct a multi-input XOR function using 2-input XORs. Nevertheless, my code worked correctly.

(the post first published at 20220722.)

List of my other blog posts.

Subscribe to my news feed

Yes, I know about these lousy Disqus ads. Please use adblocker. I would consider to subscribe to 'pro' version of Disqus if the signal/noise ratio in comments would be good enough.