I am trying to convert integer factorization to sat-3 by using a multiplication circuit. My first step is to convert the multiplication circuit into CNF.
I best understand via examples so I started with $5*7=35$. I converted it to binary.
101
111
---
101
101
101
-----
100011
And now I am trying to represent it in a generic way. For a given integer $C$ with $2n$ bits, $C=(c_1,c_2,⋯,c_{2n})$. I am interested in finding two integers $A=(a1,⋯,a_n)$ and $B=(b_1,⋯,b_n)$ whose product is $C=A∗B$.
Continuing with my example I am getting something like that:
a_3 a_2 a_1
b_3 b_2 b_1
-----------
- $c_1 = 1 = b_1 \land a_1$
- $c_2 = 1 = b_2 \land a_1 \oplus b_1 \land a_2$
- $c_3 = 0 = b_3\land a_1 \oplus b_2\land a_2 \oplus b_1\land a_3 \oplus (b_2 \land a_1 \land b_1 \land a_2)$
- $c_4 = 0 = b_3\land a_2 \oplus b_2\land a_3 \oplus (carry-on)$
- $c_5 = 0 = b_2\land a_3 \oplus (carry-on)$
- $c_6 = 1 = (carry-on)$
As you can see I got stuck with the carry-on, can you please help me to complete my example and tell me what is the general rule for it.