6 Translation Procedure

The automated translation of a logical constraint to a linear mathematical constraint in LPL is done in several steps applying various rules. Each rule is applied recursively on an (constraint) expression tree. In the following transformation procedure, the index-set i ∈{1,,n} is used for indexed expressions, the names x and y or there indexed form xi are used to denote arbitrary expressions or just variables. The letter x or vi denotes a single or indexed binary variable.

To understand the transformation procedure, the concept of a “syntax tree” and the concept of “cut-off” are introduced first. A syntax tree is a particular representation of an arbitrary (constraint) expression. Figure 1 shows the syntax trees of the following three expressions:

3 + 4 ⋅ 5 ,  (3 + 4) ⋅ 5 ,  x  ∧ (y ∨ z)

For binary operators like + (addition) or (or operator), the node (represented as a ellipse) has a left and a right child connected by an arc, for unary operators like there is only a left child (the right is a null pointer, see the node not.


Figure 1: Syntax Trees I

Indexed operators as well as function calls are considered as unary operators: See Figure 2 which represents the three syntax trees of the expressions:

∑           ∨
    x y  ,     (x ∧ y)  ,   if(a < b,x,y )
     i           i
 i           i


Figure 2: Syntax Trees II

The concept of “cut-off” is the operation of cutting a subtree off the main syntax tree. In mathematics, this operation is called “substitution”: a (sub-)expression is replaced by an additional variable as in the following expression where yz is substituted by an additional variable w :

x + yz = 17   becomes    x + w   = 17
                         w       = yz

Represented as a syntax tree, the original tree is decomposed into two (smaller) trees as shown in Figure 3, the left trees is decomposed into the two expressions on the right.


Figure 3: Cut-off a Subtree

Boolean expressions can also be cut-off. In this case, the equality sign (=) must be replaced by equivalence (). In most cases, however an implication () is sufficient. An example is given as follows with x and y being Boolean propositions and p and q are numerical (real) variables (the trees are shown in Figure 4) :

(p + q ≥ 10) ∨ x ∧ y  becomes    δ ∨ x ∧ y
                                 δ →  (p + q ≥ 10 )


Figure 4: Cut-off a Boolean Subtree

In the procedure below, a subtree containing real variables, numerical or relational operators and where the root node is not a logical operator, is called R-subtree. For example, in the left part of Figure 4, the subtree with the root of is a R-tree. The sequence in which the following steps are applied has a large influence on on how efficient the resulting expressions are. The sequence can somewhat change depending on the expressions.

  Step 0: Cut-off Subtrees
  Step 1: T0-Rules
  Step 2: T1-Rules
  Step 3: T2-Rules
  Step 4: Disconnect nested and-s
  Step 5: T3-Rules
  Step 6: Disconnect Sub-trees
  Step 7: T4-Rules