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
example .../examples/xortest.xor:
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(xor3(123, 125, 156), F)
*equ(xor(134, and3(155, 127, 167)), T)
*equ(xor(and3(1, 2, 3), and3(45, 145, 167)), F)
This may be solved using the following command:
$ sbsat xortest.xor
The result is shown in Figure 7.
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 9.4 for important details concerning this format.