patternMinor
checking '<' for two binary numbers in a cnf-formula
Viewed 0 times
numberscheckingcnftwobinaryforformula
Problem
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 < 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 < 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?
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 < 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 < 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?
Solution
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
-
$\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<m$.
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
-
$\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<m$.
Context
StackExchange Computer Science Q#116086, answer score: 3
Revisions (0)
No revisions yet.