Log Encoding Comparison inequalities

Model-level comparisons now use actual-value integer views and the selected PB provider. The bitwise construction below describes circuit logic used when binary operands are required; signed operands need sign extension rather than unconditional zero padding. See integer representations.

Overview

SATInt(a) < SATInt(b) ~> Bool
SATInt(a) <= SATInt(b) ~> Bool
SATInt(a) > SATInt(b) ~> Bool
SATInt(a) >= SATInt(b) ~> Bool

Rule Method

• Convert both operands to a canonical form by making both operands the same bit-wdith (using zero padding)
• Apply the comparison logic

Comparison Logic

For two bitvectors that have been made the same length:

$$ \begin{align} A = [a_1, a_2, \dots, a_{n}],\ B = [b_1, b_2, \dots, b_{n}] \end{align} $$

$A < B$ is equivalent to $B > A$ so we only need to encode $>$ and $\geq$, and the equivalent expression for $<$ and $\leq$ can be generated by swapping the order of the operands. There is only a slight difference between the expressions for $>$ (strict) and $\geq$ (not strict) and that is also factored in:

Shorthands

$$ \begin{align} (x > y) \equiv x \land \neg y \ (x \geq y) \equiv y \Rightarrow x \end{align} $$

Initial Case

$$ \begin{align} T_1 &= \begin{cases} a_1 > b_1 & \text{(strict)} \ a_1 \geq b_1 & \text{(non-strict)} \end{cases} \ \end{align} $$

Iteration

$$ \begin{align} T_2 &= (a_2 > b_2) \lor ((a_2 \Leftrightarrow b_2) \land T_1) \ T_3 &= (a_3 > b_3) \lor ((a_3 \Leftrightarrow b_3) \land T_2) \ \vdots \ T_{n-1} &= (a_{n-1} > b_{n-1}) \lor ((a_{n-1} \Leftrightarrow b_{n-1}) \land T_{n-2}) \ \end{align} $$

Final expression

$$ \begin{align} (A > B),\ (A \geq B) \quad \equiv \quad \boldsymbol{(b_{n} > a_{n}) \lor ((a_{n} \Leftrightarrow b_{n}) \land T_{n})} \end{align} $$

Note that in the final expression, $(a_i > b_i)$ is swapped for $(b_i > a_i)$ - this is because the sign bit should be treated inversely.