CNF Generator for Factoring Problems

Question

I've been reading these:

• Fast Reduction from RSA to SAT
• CNF Generator for Factoring Problems (Also have C code implementation)

I don't understand how the reduction from FACT to $3\text{-SAT}$ works. Are there any simple articles in which I can read about it?

My final goal is to eventually implement a reduction from $3\text{-SAT}$ to the undirected Hamiltonian circuit problem.

Answer 1

I don't understand how the reduction from FACT to 3-SAT works. Are there any simple articles in which I can read about it?

Most of the reading material assumes several steps of knowledge.

• First, you should read about how logic circuits (logic gates) work.
• Optionally learn or use a simple multiplication algorithm. You might want to start with the long-multiplication algorithm that everyone learns in school.
• Then research and understand a multiplication circuit, and/or learn how to convert the chosen algorithm to a circuit.
• You should now know how to make a simple multiplication circuit (MULT). Next learn to extend it for $n$-bit numbers.
• Once you have a circuit, you can force the outputs of the circuit to the $N$ value you want to factor. You do this by taking the $n$ outputs, and point-wise xoring them together with your $N$ value. Set the final output to be true iff $N$ and the MULT output cancel each-other out. You can do this by first oring all the xor results; if they are all $0$, then the output matched $N$ (in this case, set the final output to be $1$, else $0$).
• Now you have $\text{Circuit-SAT}$. Learn about $\text{Circuit-SAT}$.
• $\text{Circuit-SAT}$ asks if there is an input that can satisfy the output. $\text{Circuit-SAT}$ is an NP-complete problem, that is almost directly convertible to $3\text{-SAT}$ (when you get to this step, you will understand this pretty easily)
• There is a straightforward reduction from $\text{Circuit-SAT}$ to $3\text{-SAT}$ available here: Convert Circuit SAT to 3-SAT

You can't get it all in one scoop without talking to someone in-person. Rather you should follow the steps, without skipping. Each of these has "simple" material to learn from; but you'll not find one that teaches you everything in one sitting from the very basics.

---

Also see Computer Organization - Module II, section 2.5.1 Array Multiplier, which implements a carry-save-array-multiplication circuit:

Looks a lot like grade-school multiplication, doesn't it ...

Each box is (FA means "Full adder", which is also on that page in section 2.2 Serial & Parallel Adder):

Answer 2

there are several ways to conceptualize this, esp using the psychological concept of chunking which is rougly equivalent to the use of "abstraction(s)" in CS. what part is hard to understand? the conversion of factoring to SAT is much easier to understand if you learn how EE circuits implement binary arithmetic (mainly addition), and to note that multiplication is repeated addition of a shifted multiplicand, and in binary multiplication, this is reduces to bits of the multiplier simply "masking" the shifted multiplicand.

the SAT formula specifies, via a set of constraints, a relation between "input" and "output" bits equivalent to binary multiplication. it is actually like a 2-way computation device because it naturally computes in a forward direction $f(x,y)= x \cdot y = z$ and in a "reverse" (inverse) direction $f^{-1}(z)=x \cdot y$.

for multiplication implemented in SAT, specify the "input" bits, and leave "output" bits unassigned (via what are called "unit clauses") and solve the CNF formula for "output" bits. for factoring, specify the "output" bits without specifying the "input" bits.

in EE addition circuits are called "half/full adders". then the only task is to convert these circuits into SAT (CNF) formulas. binary addition of bit vectors is done most simply with a string of full adders where each carry bit feeds into the next stage of the addition, the so-called "ripple carry adder".

here is a nice slideshow on converting binary/bitvector arithmetic to propositional logic aka "bitblasting". on slide 8 the CNF formula for a full adder is given. slide 10 has the same ripple carry adder.

• Bit vector logic
• full adder, wikipedia