# Some Tips of Implementing Order Encoding

## Outline

In the order encoding, a comparison $$x \le a$$ (alternatively $$x \ge a$$) is encoded by a different Boolean variable for each integer variable $$x$$ and integer value $$a$$. It is first used by Crawford and Baker to encode Job-shop scheduling problems, and extended to the finite-domain linear CSP (Constraint Satisfaction Problems). This encoding is proved to translate tractable CSP to tractable SAT by Justyna Petke and Peter Jeavons.

There are some important related works. Regular encoding uses $$x \ge a$$ to encode integer variables (but not arithmetic constraints). Unary number representation is used by several researchers in encoding Boolean cardinality constraints and Pseudo Boolean constraints.

## Preliminaries

• $$lb(E)$$ denotes the lower bound value of the expression $$E$$.
• $$ub(E)$$ denotes the upper bound value of the expression $$E$$.

## Naive Implementation

### Algorithm

This is a naive implementation of the order encoding described in the paper Compling finite linear CSP into SAT.

When encoding $$\sum_{i=1}^n a_i x_i \le c$$, basically the following loop is performed.

for (b1 <- lb(a1*x1)-1 to ub(a1*x1)) {
for (b2 <- lb(a2*x2)-1 to ub(a2*x2)) {
...
for (bn <- lb(an*xn)-1 to ub(an*xn)) {
if (b1+b2+...+bn == c-n+1) {
generate_clause
}
}
...
}
}


For each loop, a clause $$\bigvee_{i=1}^n (a_i x_i \le b_i)^\#$$ is generated where $$(a x \le b)^\#$$ is defined as follows. \begin{eqnarray*} (ax \le b)^\# & = & \left\{\begin{array}{ll} x \le \left\lfloor\frac{b}{a}\right\rfloor & (a > 0) \\ \neg\left(x \le \left\lceil\frac{b}{a}\right\rceil-1\right) & (a < 0) \end{array}\right. \end{eqnarray*}

### Program

See OrderEncoding0.scala program written in Scala language.

• Var(name: String, lb: Int, ub: Int) is a class for integer variables. lb and ub are its lower and upper bound values respectively.
• P(x: Var, b: Int) a class for propositional variables meaning $$x \le b$$. It is interpreted as false when $$b < lb(x)$$, and as true when $$b \ge ub(x)$$.
• Literal(p: Bool, neg: Boolean) is a class for literals where neg is a negative sign.
• Clause(lits: Seq[Literal]) is a class for clauses where lits is a sequence of literals.
• Function lb(a: Int, x: Var) returns the lower bound value $$ax$$.
• Function ub(a: Int, x: Var) returns the upper bound value $$ax$$.
• Function lb(wsum: Seq[(Int,Var)]) returns the lower bound value of the weighted sum wsum.
• Function ub(wsum: Seq[(Int,Var)]) returns the upper bound value of the weighted sum $$\sum a_i x_i$$ when wsum is a sequence of pairs $$(a_i,x_i)$$.
• Function floorDiv(b: Int, a: Int) returns the value $$\lfloor\frac{b}{a}\rfloor$$.
• Function ceilDiv(b: Int, a: Int) returns the value $$\lceil\frac{b}{a}\rceil$$.
• Function p(x: Var, b: Int) returns a propositional variable P(x, b) when $$lb(x) \le b < ub(x)$$. It returns false when $$b < lb(x)$$, and returns true when $$b \ge ub(x)$$.
• Function le(a: Int, x: Var, b: Int) returns a literal obtained by encoding $$ax \le b$$.
• Function encodeLe(wsum: Seq[(Int,Var)], c: Int) returns a sequence of clauses obtained by encoding a linear comparison $$\sum a_i x_i \le c$$ when wsum is a sequence of pairs $$(a_i,x_i)$$.

### Example 1

Encoding $$x + y \le 7$$ when $$x, y \in \{2..6\}$$.

$scalac OrderEncoding0.scala$ scala
scala> OrderEncoding0.example1
{P(y,5)}
{P(x,2), P(y,4)}
{P(x,3), P(y,3)}
{P(x,4), P(y,2)}
{P(x,5)}
5 clauses


### Example 2

Encoding $$x + y < z - 1$$ when $$x, y, z \in \{0..3\}$$.

scala> OrderEncoding0.example2
{-P(z,1)}
{P(y,0), -P(z,2)}
{P(y,1)}
{P(x,0), -P(z,2)}
{P(x,0), P(y,0)}
{P(x,1)}
6 clauses


### Example 3

Encoding $$3x + 5y \le 14$$ when $$x, y \in \{0..5\}$$.

scala> OrderEncoding0.example3
{P(y,2)}
{P(x,0), P(y,2)}
{P(x,0), P(y,2)}
{P(x,0), P(y,2)}
{P(x,1), P(y,2)}
{P(x,1), P(y,1)}
{P(x,1), P(y,1)}
{P(x,2), P(y,1)}
{P(x,2), P(y,1)}
{P(x,2), P(y,1)}
{P(x,3), P(y,0)}
{P(x,3), P(y,0)}
{P(x,3), P(y,0)}
{P(x,4), P(y,0)}
{P(x,4), P(y,0)}
{P(x,4)}
16 clauses

• This result contains a lot of redundant clauses.

## Looping by Variable Values

### Algorithm

When encoding $$\sum_{i=1}^n a_i x_i \le c$$, the following algorithm generates much less clauses than the naive implementation.

• When $$a_1 > 0$$, do the following for each $$b \in \{lb(x_1)..ub(x_1)+1\}$$.
• If we assume $$x_1 \ge b$$, then $$\sum_{i=2}^n a_i x_i \le c - ab$$. Therefore, recursively encode $$\sum_{i=2}^n a_i x_i \le c - ab$$ and add a literal $$x_1 \le b-1$$ for each clause.
• When $$a_1 < 0$$, do the following for each $$b \in \{lb(x_1)-1..ub(x_1)\}$$.
• If we assume $$x_1 \le b$$, then $$\sum_{i=2}^n a_i x_i \le c - ab$$. Therefore, recursively encode $$\sum_{i=2}^n a_i x_i \le c - ab$$ and add a literal $$\neg(x_1 \le b)$$ for each clause.

### Program

See OrderEncoding1.scala program written in Scala language.

### Example 3

Encoding $$3x + 5y \le 14$$ when $$x \in \{0..5\}$$ and $$y \in \{0..3\}$$.

scala> OrderEncoding1.example3
{P(y,2)}
{P(x,0), P(y,2)}
{P(x,1), P(y,1)}
{P(x,2), P(y,1)}
{P(x,3), P(y,0)}
{P(x,4)}
6 clauses


## Sorting Variables

Sorting variables in weighted sums can improve the encoding performance.

• Choose variable with smaller domain size first.
• Choose variable whose coefficient has larger absolute value first.

### Example 4

Encoding $$3x + 5y \le 14$$ when $$x \in \{0..5\}$$ and $$y \in \{0..3\}$$ after sorting the variables in the weighted sum.

scala> OrderEncoding1.example4
{P(x,4)}
{P(y,0), P(x,3)}
{P(y,1), P(x,1)}
{P(y,2)}
4 clauses


## Decomposing Weighted Sum

Decomposing weighted sum by introducing auxiliary variables can improve the encoding performance. For example, $$w+x+y+z \le c$$ requires $$O(d^3)$$ clauses where $$d$$ is the domain size of variables. Whereas, $$w+x+u \le c \land y+z-u \le 0 \land -y-z+u \le 0$$ requires $$O(d^2)$$ clauses.

### Example 5

Encoding $$w + x + y + z \le 200$$ when $$w,x,y,z \in \{0..99\}$$.

scala> OrderEncoding1.example5
665812 clauses


### Example 6

Encoding $$w + x + u \le 200 \land y + z - u \le 0 \land - y - z + u \le 0$$ when $$w,x,y,z \in \{0..99\}$$ and $$u \in \{0..198\}$$.

scala> OrderEncoding1.example6
19993 clauses


## Non-contiguous Domain Values

Some CSP variables take non-contiguous values in CSP solver competition benchmarks.

Suppose the domain of variable $$x$$ is $$\mbox{dom}(x) = \{d_1,d_2,\ldots,d_n\}$$ and $$d_1 < d_2 < \cdots < d_n$$. It is sufficient to assign propositional variables for each $$x \le d_j$$ ($$1 \le j < n$$) instead of assigning for each value $$d$$ where $$d_1 \le d < d_n$$.

### Algorithm (should be checked…)

The following algorithm shows how to encode $$\sum_{i=1}^n a_i x_i \le c$$.

• When $$a_1 > 0$$, do the following for each $$b \in \mbox{dom}(x_1)$$.
• If we assume $$x_1 \ge b$$, we get $$\sum_{i=2}^n a_i x_i \le c - ab$$. Therefore, recursively encode $$\sum_{i=2}^n a_i x_i \le c - ab$$ and add a literal $$x_1 \le b-1$$ for each clause.
• Note that when $$\mbox{dom}(x_1) = \{d_1,d_2,\ldots,d_n\}$$ and $$b = d_j$$ for some $$j > 0$$, $$x_1 \le b-1$$ is equivalent to $$x_1 \le d_{j-1}$$. Also it is equivalent to false when $$b = d_1$$.
• When $$a_1 < 0$$, do the following for each $$b \in \mbox{dom}(x_1)$$.
• If we assume $$x_1 \le b$$, we get $$\sum_{i=2}^n a_i x_i \le c - ab$$. Therefore, recursively encode $$\sum_{i=2}^n a_i x_i \le c - ab$$ and add a literal $$\neg(x_1 \le b)$$ for each clause.
• Note that $$\neg(x_1 \le b)$$ is equivalent to false when $$b = d_n$$.

### Program

See OrderEncoding2.scala program written in Scala language.

### Example 7

Encoding $$x + y \le 20$$ when $$x,y \in \{0, 10, 20\}$$.

scala> OrderEncoding2.example7
{P(x,0), P(y,10)}
{P(x,10), P(y,0)}
2 clauses


### Example 8

Encoding $$x + y - 2z \le 20$$ when $$x,y,z \in \{0, 10, 20\}$$.

scala> OrderEncoding2.example8
{-P(z,0), P(x,0), P(y,10)}
{-P(z,0), P(x,10), P(y,0)}
3 clauses


## TODO Bounds Consistency at Preprocessing

Date: 2013-12-24 23:56:45 JST

Validate XHTML 1.0