5
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ The formula should express the following: there is some $\ell$ such that the first $\ell$ digits are the same, and the following digits of $n,m$ are $0,1$, respectively. $\endgroup$ – Yuval Filmus Oct 21 '19 at 19:47
3
$\begingroup$

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 < 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<m$.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ @AlbertHendriks, thanks for the corrections! I've updated my answer accordingly. $\endgroup$ – D.W. Oct 23 '19 at 0:46
0
$\begingroup$

I want to check whether a arbitrary binary number is less or equal to another binary number in a cnf-formula.

This exercise is very interesting to become familiar with Boolean formulas in CNF. In the question you did not specify whether the two numbers must have the same length or different lengths but for simplicity we will focus on the case $|n|=|m|$. When we are done, you will notice that the cases $|n|<|m|$ and $|m|<|n|$ are "trivial" variation of the former, which is more interesting. Let's see some properties that the formula you requested has, first of all a bit of combinatorics; we will build up the truth table of your formula $\phi$ for $1$, $2$ and $3$-bit numbers.

$1$-bit truth table $\begin{bmatrix} 0_{(mn00)} & 0_{(mn01)} \\ \color{red}{\text{1}}_{(mn10)} & 0_{(mn11)} \\ \end{bmatrix}$


$2$-bit truth table $\begin{bmatrix} 0_{(00|00)} & 0_{(00|01)} & 0_{(00|10)} & 0_{(00|11)}\\ \color{red}{\text{1}}_{(01|00)} & 0_{(01|01)} & 0_{(01|10)} & 0_{(01|11)}\\ \color{red}{\text{1}}_{(10|00)} & \color{red}{\text{1}}_{(10|01)} & 0_{(10|10)} & 0_{(10|11)}\\ \color{red}{\text{1}}_{(11|00)} & \color{red}{\text{1}}_{(11|01)} & \color{red}{\text{1}}_{(11|10)} & 0_{(11|11)}\\ \end{bmatrix}$


$3$-bit truth table

$\begin{bmatrix} 0_{(000|000)} & 0_{(000|001)} & 0_{(000|010)} & 0_{(000|011)}& 0_{(000|100)} & 0_{(000|101)} & 0_{(000|110)} & 0_{(000|111)} \\ \color{red}{\text{1}}_{(001|000)} & 0_{(001|001)} & 0_{(001|010)} & 0_{(001|011)} & 0_{(001|100)} & 0_{(001|101)} & 0_{(001|110)} & 0_{(001|111)}\\ \color{red}{\text{1}}_{(010|000)} & \color{red}{\text{1}}_{(010|001)} & 0_{(010|010)} & 0_{(010|011)} & 0_{(010|100)} & 0_{(010|101)} & 0_{(010|110)} & 0_{(010|111)}\\ \color{red}{\text{1}}_{(011|000)} & \color{red}{\text{1}}_{(011|001)} & \color{red}{\text{1}}_{(011|010)} & 0_{(011|011)} & 0_{(011|100)} & 0_{(011|101)} & 0_{(011|110)} & 0_{(011|111)}\\ \color{red}{\text{1}}_{(100|000)} & \color{red}{\text{1}}_{(100|001)} & \color{red}{\text{1}}_{(100|010)} & \color{red}{\text{1}}_{(100|011)} & 0_{(100|100)} & 0_{(100|101)} & 0_{(100|110)} & 0_{(100|111)}\\ \color{red}{\text{1}}_{(101|000)} & \color{red}{\text{1}}_{(101|001)} & \color{red}{\text{1}}_{(101|010)} & \color{red}{\text{1}}_{(101|011)} & \color{red}{\text{1}}_{(101|100)} & 0_{(101|101)} & 0_{(101|110)} & 0_{(101|111)}\\ \color{red}{\text{1}}_{(110|000)} & \color{red}{\text{1}}_{(110|001)} & \color{red}{\text{1}}_{(110|010)} & \color{red}{\text{1}}_{(110|011)} & \color{red}{\text{1}}_{(110|100)} & \color{red}{\text{1}}_{(110|101)} & 0_{(110|110)} & 0_{(110|111)}\\ \color{red}{\text{1}}_{(111|000)} & \color{red}{\text{1}}_{(111|001)} & \color{red}{\text{1}}_{(111|010)} & \color{red}{\text{1}}_{(111|011)} & \color{red}{\text{1}}_{(111|100)} & \color{red}{\text{1}}_{(111|101)} & \color{red}{\text{1}}_{(111|110)} & 0_{(111|111)}\\ \end{bmatrix}$

In the previous tables I have highlighted in red the cases in which $\phi = 1$ ($n<m$). An interesting thing about this function is the fact that the more $n$ and $m$ increase in the number of bits, the closer the number of valid results by random assignements approximates to $\frac{1}{2}$, this is a convergent series:

$Pr(\phi =1)$ (with $|n|$=$|m|$=$1$ bit): $0,25$

$Pr(\phi =1)$ (with $|n|$=$|m|$=$2$ bits): $0,375$

$Pr(\phi =1)$ (with $|n|$=$|m|$=$3$ bits): $0,4375$

$Pr(\phi =1)$ (with $|n|$=$|m|$=$5$ bits): $0,484375$

$Pr(\phi =1)$ (with $|n|$=$|m|$=$6$ bits): $0,4921$

$Pr(\phi =1)$ (with $|n|$=$|m|$=$14$ bits): $0,499969$

$Pr(\phi =1)$ (with $|n|$=$|m|$=$20$ bits): $0,4999995$

The diagonal of the truth matrix is ​​always composed entirely by $0$s, below that we find the values ​​that validate the formula, above those that invalidate it. If $|n|>|m|$ there is an increase in $0$s, if instead $|m|>|n|$ there is an increase in $1$s.

Obviously, the longer the length of $n$ and $m$, the longer the length of the formula. It is impossible to have a boolean formula that does what you ask but that is of fixed size. Let's see how the CNF looks for the simplest case (the first truth table), $|n|=|m|=1$bit :

$\phi$ = ($\neg n$ $\lor$ $\neg n$) $\land$ ($m$ $\lor$ $m$)

$\phi$ is validated if and only if $n$ < $m$ when $n$ and $m$ are $1$ bit long.

I hope that what is written above can help you by giving you more tools to "visualize" and build the formula according to your needs.

| cite | improve this answer | |
$\endgroup$
  • 4
    $\begingroup$ I don't see how this answers the question. This looks like an extended comment with musings related to the question, but it does not appear to directly answer the question. In particular, the question is how to construct a CNF formula; and this does not describe how to construct a CNF formula. We prefer that you reserve the 'Your Answer' box only for material that directly answers the question. If there is something I am missing, I encourage you to edit your answer to make it clear how it directly answers the question that was asked. $\endgroup$ – D.W. Oct 22 '19 at 20:07
  • 1
    $\begingroup$ @D.W. you are right, this would belong to a comment but being rather verbose I could not write and format everything in a simple comment. let me know if I have to delete the answer or if I can leave it because it can provide some context to the question. $\endgroup$ – Yamar69 Oct 23 '19 at 7:12
  • $\begingroup$ @Yamar69 Since the question seems to have been answered to the OPs satisfaction, is your comment still relevant? Can you expand it into an answer? $\endgroup$ – Raphael Oct 30 '19 at 21:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.