Rules:

• A blank is either a space or a tab character. Items are separated by at least one blank. Leading and trailing blanks are allowed everywhere.
• The first line of an instance starts with the keyword START. All preceding lines in the input file are skipped and can be used for comments.
• The last line of an instance must consist of the keyword END.
• Each line between START and END is of the type KEY FORMULA.
  • If KEY is a real (in fixed or floating-point representation) or an integer, it is the weight of FORMULA in the objective function (assuming maximization)
  • If KEY is C0, then FORMULA must be false for every feasible solution
  • If KEY is C1, then FORMULA must be true for every feasible solution
  • If KEY is CS, then FORMULA must be of the form F1 ; F2 ; … ; Fk, where all Fi are formulae of which at most one may be true for every feasible solution
  • If KEY is CE, then FORMULA must be of the form F1 ; F2 ; … ; Fk, where all Fi are formulae of which exactly one may be true for every feasible solution
• A formula F is either a basic variable (a string of at most 25 alfa-numeric characters) or recursively defined by other formulae F1 and F2 according to one of the following rules:
  • (!F1), meaning F1 negated
  • (F1) & (F2), meaning F1 and F2
  • (F1) | (F2) , meaning F1 or F2
  • (F1) ^ (F2) , meaning F1 or F2 but not both
  • (F1) = (F2) , meaning F1 and F2 are equivalent
  • (F1) > (F2) , meaning F1 implies F2
  • (F1) < (F2) , meaning F1 is implied by F2

Note: Parentheses are not mandatory. If missing, the precedence among binary operators is based on their position in the formula, and operators are applied from right to left.

Example:

a <op1> b <op2> c <op3> d <op4> e

is equivalent to

a <op1> (b <op2> (c <op3> (d <op4> e)))

The unary operator ! always applies to the formula immediately following to the right

Example:

a <op1> ! b <op2> c <op3> d <op4> e is equivalent to a <op1> ! (b <op2> (c <op3> (d <op4> e)))

Note: There are no predefined constants like 1, or 0, or TRUE, or FALSE. Actually, a numeric string-like, e.g., “1” is taken as the name of a variable. If one wants to use the constant 1, or the constant FALSE, then it is necessary to assign these variable names a value using the KEY”s C0 or C1. For example, if the strings “1” and “FALSE” are to be intended as the constants 1 and 0, then two of the lines must be

C1 1

C0 FALSE

Example: 

maximize (gt0 => (v1 or v2)) + ((gt0 xor gt1) <=> v3))
-1.2 v1 -2.5 (!v2) -3.0 v3 +5.0 gt
subject to (gt => (gt0 or gt1))

Input file:

Logic Optimization Instance
START
1    gt0 > (v1 | v2)
1    (gt0 ^ gt1) = v3
-1.2 v1
-2.5 !v2
-3.0 v3
5.0  gt
C1   gt > (gt0 | gt1)
END