Download SBSAT User Manual and Quick Start Guide

of 0 (1) represents an assignment of F (T). An example of a function section
with a truth table is the following:
2
8 9 2 4 -1
1001011011110000
This function has a value F if, for example, variable 8 has value T and variables
2,9, and 4 have value F. This function has value T if, for example, variables 2
and 8 have value T and variables 4 and 9 have value F.
Another possible format for the third line of a function section is the specification of a function identifier and polarity list. The intention of this format is
to allow compact specification of commonly used functions (especially in circuit
problems) with quite a few arguments that would otherwise require extremely
large truth tables. Function identifiers accepted are: and=, or=, and plainor.
The identifier plainor correspond to the “or” function described in Section 2.2.
Identifiers with = equate a single variable on the left of the = with a simple
expression on the right of the type indicated by the identifier. For example,
and= corresponds to a function of the form:
<var> = and(<var>, ...
<var>)
This function has value T if and only if the value of the variable on the left of =
is the same as the logical “and” of the variables on the right of =. For identifiers
with =, the polarity list is a string of characters from the set {0 , 1 , 3 } with
exactly one 3. The number of characters is the number of variables identified
on the second line of the function section and each character corresponds to
an input variable: the leftmost character corresponding to the leftmost input
variable. The ’3’ identifies the input variable that is on the left side of =. The
remaining 0’s and 1’s determine the polarity of the variables on the right side
of =. An example of a function section with function identifier containing = is
the following:
41
4 11 12 186 187 188 189 193 382 -1
and= 011000031
This would be identical to the following:
193 = and(-4, 11, 12, -186, -187, -188, -189, 382)
67