**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