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.