checking '<' for two binary numbers in a cnf-formula
Yuval describes the general approach.

Let the binary representation of the two numbers be $n_1,\dots,n_k$ and $m_1,\dots,m_k$, where $n_1$ is the most significant bit.  Introduce fresh new boolean variables $t_1,\dots,t_k$.  The intention is that these will indicate the common prefix of $n,m$.

In particular, add the following clauses:


$t_{i+1} \implies t_i$ -- this ensures that $t_1,\dots,t_k$ has the form $1,\dots,1,0,\dots,0$.
$t_i \implies (n_i=m_i)$ -- this ensures that $t_1,\dots,t_k$ captures the common prefix of $n,m$
$(t_{i-1} \land \neg t_i) \implies (n_i=0 \land m_i=1)$ -- this ensures that at the first position where $n,m$ differ, $n_i &lt; m_i$.  (For the case $i=1$, treat $t_{i-1}$ as True.)
$\neg t_k$ -- this ensures $n \ne m$


Each of these can be converted to a conjunction of CNF clauses.  For instance, the first corresponds to the CNF clause $\neg t_{i+1} \lor t_i$.  The second corresponds to $(\neg t_i \lor \neg n_i \lor m_i) \land (\neg t_i \lor n_i \lor \neg m_i)$.  The third corresponds to $(\neg t_{i+1} \lor t_i \lor \neg n_i) \land (\neg t_{i+1} \lor t_i \lor m_i)$.

Now your formula is the conjunction of all of these CNF clauses.  You obtain a formula with about $5k$ clauses.  This formula will be satisfiable iff $n&lt;m$.