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 preceeding 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)))

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