next up previous contents
Next: Reusing functions (Macros) Up: Quick Start - The Previous: An input in canonical   Contents

An input in XOR format

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(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.

John Franco 2011-09-15