The XOR format is a specialization of the canonical form allowing
up to two levels of function nesting. However, the grammar of this
format is very different. The following is the
p xor 12 3
x123 x125 x156 = 0
x134 x155x127x167 = 1
x1x2x3 x45x145x167 = 0
which is equivalent to the following canonical form
p bdd 12 3
equ(xor(123, 125, 156), F)
equ(xor(134, and(155, 127, 167)), T)
equ(xor(and(1, 2, 3), and(45, 145, 167)), F)
This may be solved using the following command:
$ sbsat xortest.xor
The result is shown in Figure .
One peculiarity of this format is that all variables must have names that begin with x and end with a number. No other variable names are allowed. See Section for important details concerning this format.