Some Tips of Implementing Order Encoding

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

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)\).

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

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

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.

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.

See OrderEncoding1.scala program written in Scala language.

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

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

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

scala> OrderEncoding1.example5
665812 clauses

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

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\).

See OrderEncoding2.scala program written in Scala language.

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

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