next up previous contents
Next: Trace format Up: XOR format Previous: File Header   Contents

Boolean functions

Each line of the file is a function. Each line has the following form:

<grouping> ... <grouping> = [0|1]

where <grouping> has the form


and <variable> has the form


where <number> is a positive integer no greater than <max-var-number>. The following are examples:

x1 x2 x3 = 1
x1x2x3 = 1
x1x2x3 x2x3 x4x5x6 = 0

sbsat interprets a line as an xor of conjunctions, each consisting of variables identified in a <grouping>. The following table shows the above as expressions in canonical form:

This ... is equivalent to this
x1 x2 x3 = 1 equ( xor(1, 2, 3), T)
x1x2x3 = 1 equ( and(1, 2, 3), T)
x1x2x3 x2x3 x4x5x6 = 0 equ(xor(and(1, 2, 3), and(2, 3), and(4, 5, 6)), F)

John Franco 2011-09-15