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.