Python Program for Evaluation Logic Formulas Generated by Lsquare Program
by Matthias Granberry
email: matthias@utdallas.edu
The process of converting True/False values of the variables to an
integer must currently be done manually, but the logic_formula_eval.py script
will generate C or Java code to evaluate a logic formula from the
lsqcc-generated .cut file. The two processes are described below:
The leibniz system assigns each variable a number from 1 to the number
of variables, inclusive. A value of True (resp. False) for a logic
variable is encoded as a 1 (resp. 0) in the bit positon corresponding
to the number assigned to the variable by the Leibniz system. If a
variable X is assigned to position 1 by the Leibniz system and Y is
assigned to position 2, then a value of True for X and False for Y
would be encoded by the number ((1 << 0) | (0 << 1)) or 1 would be the
resulting integer.
To encode a clause, two integers M+/- and M+ are constructed. A bit
in M+/- corresponding to a literal's number is set to 1 if there is a
True or False for the literal in the clause. Otherwise, the bit in
that position is set to 0. M+ is the same, but a bit is set to 1 only
if the literal is True in the clause. The expression
((formula & M+/-) == M+) evaluates to True/False in the same manner as a naive
implementation, but with only a single bitwise AND (&) and one comparison (==).
Several clauses are then boolean ORed (||) together in an if statement that
votes for A or B, depending on the formula type.
As an example, consider the following portion of a file face.sep:
Formula 1 B 2 min (True means vote for B, 2 min size clause(s))
clause size literals
1 1 -7
2 2 -6 -17
Logic notation
[ -U2_1 ] |
[ -V1_1 & -V4_1 ]
Formula 3 A 2 min (True means vote for A, 2 min size clause(s))
clause size literals
1 1 5
2 2 -15 18
Logic notation
[ U1_5 ] |
[ -U4_3 & U5_1 ] |
The command 'python sep2code.py face.sep' gives the following output:
if ( ((formula & ( 16 )) == ( 16 ))
|| ((formula & ( 147456 )) == ( 131072 ))
) {vote++;} else vote--;
if ( ((formula & ( 64 )) == ( 0 ))
|| ((formula & ( 65568 )) == ( 0 ))
) {vote--;} else vote++;
The formulas that vote for A when they evaluate to True are presented
first, followed by those which vote for B when they evaluate to True.
The generated code relies on two variables: formula, which is
initalized as described earlier, and vote, which must be set to 0 before
the generated code is inserted.