Some Tips of Implementing Order Encoding

Table of Contents

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 Tseitin Transformation

TODO Non-linear Constraints

TODO Decomposing Global Constraints

TODO Extensional Constraints

TODO Bounds Consistency at Preprocessing

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

Author: Naoyuki Tamura

Validate XHTML 1.0