checking '<' for two binary numbers in a cnf-formula I want to check whether a arbitrary binary number is less or equal to another binary number in a cnf-formula. I can already construct a formula, which is not in cnf:

Lets say n and m are two-digit binary numbers:

$n = n_2 + n_1$

$m = m_2 + m_1,$

where $n_i, m_i \in \{0,1\}$ for $i \in \{1,2\}$. Then the boolean formula, which will evaluate to true if $n &lt; m$, would be:

$(\neg n_2 \land m_2) \lor (((\neg n_2 \land \neg m_2) \lor (n_2 \land m_2)) \land \neg n_1 \land m_1)$

As described, this formula should only evaluate to true if $n &lt; m$. I know that every boolean formula can be transformed into a cnf formula, but it seems impractical, if i have higher digit binaries.

So is there a way to construct a cnf formula, which does the same?
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$.