Deriving a multiplication circuit for the Prime Factorization problem is trivial if you know how to convert the arithmetic and relational expressions into propositional logic. Below I will show few expressions and their corresponding CNF formulation.

#### Converting Arithmetic and Relational expressions to Propositional Logic

Here symbols such as x, y, z, a, b, c etc... each denote a single boolean value that can take either true or false value.

We use ≠ to represent inequality, and ! to denote logical Not. The sign = is used to denote equality (and not assignment). Thus it is same as == of C/C++; For example, the expression if x then y=1 means whenever x is true, y also should be true, which is same as if x then assert(y==1) in C++.

For CNF expressions we use to represent logical AND, to represent logical OR, and - to represent complement. Thus x and -(-(x)) should essentially mean the same.

 Expression CNF if x then y=1 (-x ∨ y) if x then y=0 (-x ∨ -y) x ≥ y (x ∨ -y) x ≤ y (-x ∨ y) x = y (-x ∨ y) ∧ (x ∨ -y) x ≠ y (x ∨ y) ∧ (-x ∨ -y) x > y (x ∨ y) ∧ (x ∨ -y) ∧ (-x ∨ -y) x < y (x ∨ y) ∧ (-x ∨ y) ∧ (-x ∨ -y) (x & y) = z (-x ∨ -y ∨ z) ∧ (x ∨ -z) ∧ (y ∨ -z) if(x) then (a = b) (-x ∨ a ∨ -b) ∧ (-x ∨ -a ∨ b) if(x) then (a ≠ b) (-x ∨ a ∨ b) ∧ (-x ∨ -a ∨ -b) if(!x) then (a = b) (x ∨ a ∨ -b) ∧ (x ∨ -a ∨ b) if(!x) then (a ≠ b) (x ∨ a ∨ b) ∧ (x ∨ -a ∨ -b) if(x & y) then (a = b) (-x ∨ -y ∨ a ∨ -b) ∧ (-x ∨ -y ∨ -a ∨ b) if(!x & !y) then (a = b) (x ∨ y ∨ a ∨ -b) ∧ (x ∨ y ∨ -a ∨ b) if(x = y) then (a = b) (-x ∨ -y ∨ -a ∨ b) ∧ (-x ∨ -y ∨ a ∨ -b) ∧ (x ∨ y ∨ a ∨ -b) ∧ (x ∨ y ∨ -a ∨ b)

Once we have the understanding of above conversions, we can start building complex circuits such as Adder, Bit-shifter etc... easily.

#### CNF Expression for Full-Adder

```          |i (Carry-in)
|
|‾‾‾‾‾|
x-----|     |----S (Sum)
| F A |
y-----|_____|----C (Carry-out)
```

In the above full-adder, inputs are x, y and i, while the outputs are s and c. Equations are as below:

S ≡ (x + y + i) % 2 ≡ x ⊕ y ⊕ i;

C ≡ (x + y + i) / 2 ≡ x.y + x.i + y.i;

CNF for the Carry-out is:

(x ∨ y ∨ -c) ∧ (x ∨ i ∨ -c) ∧ (y ∨ i ∨ -c) ∧ (-x ∨ -y ∨ c) ∧ (-x ∨ -i ∨ c) ∧ (-y ∨ -i ∨ c)

CNF for the Sum is:

(x ∨ y ∨ i ∨ -s) ∧ (x ∨ -y ∨ -i ∨ -s) ∧ (-x ∨ y ∨ -i ∨ -s) ∧ (-x ∨ -y ∨ i ∨ -s) ∧ (-x ∨ -y ∨ -i ∨ s) ∧ (-x ∨ y ∨ i ∨ s) ∧ (x ∨ -y ∨ i ∨ s) ∧ (x ∨ y ∨ -i ∨ s)

#### Multiplier Circuit in DIMACS CNF for Prime Factorizaion

Once we have the CNF expressions for the sum and carry of Full adder, we can use them to create the CNF expression for the Multiplier circuit for Prime Factorization problem. Given a product in n bits, we need to express it as the product of two numbers that take no more than (n+1)/2 bits. We can create a simple class to take care of the carry, sum and the factors A, B variable numberings as shown below:

```// Class to compute the variable indices for the A, B, Carry and Sum
class CVariables
{
int nBits;	// Number of bits in the product
int nBitsBy2;	// nBitsBy2 == (nBits+1)/2
TwoDimArray _c;	// Holds the Var indices for Carry
TwoDimArray _s;	// Holds the Var indices for Sum
Array _p;	// Holds the product bits
public:
inline CVariables(const char* pBits, int n) : nBits(n), nBitsBy2((n+1)/2)
{
_c.ReDim(nBitsBy2+1, n+1);
_s.ReDim(nBitsBy2+1, n+1);
_p.ReDim(n+1);

// for each column upto last column
for(int j=2, nCount=0; j < n; ++j)
{
// for each row
for(int i=2; i <= nBitsBy2; ++i)
{
_c(i, j) = C_Start() + nCount++;
if(i==j) break;
}
}

// for each column upto last column
for(int j=2, nCount=0; j <= n; ++j)
{
// for each row upto the middle
for(int i=2; i < nBitsBy2; ++i)
{
if(i==j) break;
_s(i, j) = S_Start() + nCount++;
}
}

// Extract the product bits
for(int nIndex=n; *pBits != '\0'; ++pBits, nIndex--)
{
switch(*pBits)
{
case '0': _p(nIndex) = 0;  break;
case '1': _p(nIndex) = 1; break;
default: fprintf(stderr, "\nInvalid Product bit: %c", *pBits); return;
}
}
}

inline int A_Start() const  { return 1;	}
inline int A_Length() const { return nBits;	}
inline int A_End() const	{ return A_Length(); }

inline int B_Start() const	{ return A_End() + 1;	}
inline int B_Length() const	{ return nBitsBy2;	}
inline int B_End() const	{ return B_Start() + B_Length() -1;	}

inline int C_Start() const	{ return B_End() + 1;	}
inline int C_Length() const { return (nBits*(nBitsBy2-1)) - (nBitsBy2*(nBitsBy2-1)/2) - (nBitsBy2-1);	}
inline int C_End() const	{ return C_Start() + C_Length() -1; }

inline int S_Start() const	{ return C_End() + 1;	}
inline int S_Length() const	{ return (nBits*(nBitsBy2-2)) - ((nBitsBy2-2)*(nBitsBy2-1)/2) - (nBitsBy2-2);	}
inline int S_End() const	{ return S_Start() + S_Length() - 1; }

inline int A(int nIndex) const
{
//_ASSERTE(nIndex >= 1 && nIndex <= nBits);
return A_Start() + (nIndex-1);
}

inline int B(int nIndex) const
{
//_ASSERTE(nIndex >= 1 && nIndex <= nBitsBy2);
return B_Start() + (nIndex-1);
}

inline int C(int i, int j) const
{
//_ASSERTE(i >= 2 && i <= nBitsBy2 && j>=1 && j <=nBits);
return _c(i, j);
}

inline int S(int i, int j) const
{
//_ASSERTE(i >= 2 && i <= nBitsBy2 && j>=1 && j <=nBits);
return _s(i, j);
}

inline int P(int nIndex) const { return _p(nIndex); }
};
```

Once we have this, we can go ahead and write the multiplier circuit as below:

```// Returns the number of clauses written
int PrintMultiplicationTable(FILE* fp, const CVariables& var)
{
int i, j;
int jMax = var.A_Length(); // n
int iMax = var.B_Length(); // (n+1)/2
int Svar;	// Variable that holds the column wise sum upto now
int nClauseCount = 0;

// for each column upto last column
for(j=2; j < jMax; ++j)
{
Svar = var.A(j);

for(i=2; i < iMax; ++i)	// for each row upto the middle
{
if(i == j) break;

nClauseCount += PrintSum(fp, Svar, var.B(i), var.A(j-i+1), var.C(i, j-1), var.S(i, j));

nClauseCount += PrintCarry(fp, Svar, var.B(i), var.A(j-i+1), var.C(i, j-1), var.C(i, j));

Svar = var.S(i, j);
}

if(i == j)	// Did we reach down a1 ??
{
if(var.P(j) == 1)
nClauseCount += PrintSum1(fp, Svar, var.B(i));
else if(var.P(j)==0)
nClauseCount += PrintSum0(fp, Svar, var.B(i));

nClauseCount += PrintCarry(fp, Svar, var.B(i), var.C(i, j)); // A(j)=1 Cin=0
}
else	// We have not reached upto a1
{
if(var.P(j)==1)
nClauseCount += PrintSum1(fp, Svar, var.B(i), var.A(j-i+1), var.C(i, j-1));
else if(var.P(j)==0)
nClauseCount += PrintSum0(fp, Svar, var.B(i), var.A(j-i+1), var.C(i, j-1));

nClauseCount += PrintCarry(fp, Svar, var.B(i), var.A(j-i+1), var.C(i, j-1), var.C(i, j));
}
}

// here j==n;  Take care of the last column now. For this column we dont have any carry-outs.
Svar = var.A(j);	// Value of A[n] usually is FALSE

for(i=2; i < iMax; ++i)
{
if(i == j) break;

nClauseCount += PrintSum(fp, Svar, var.B(i), var.A(j-i+1), var.C(i, j-1), var.S(i, j));

nClauseCount += PrintCarry0(fp, Svar, var.B(i), var.A(j-i+1), var.C(i, j-1));

Svar = var.S(i, j);
}
if(i == j)
_ASSERTE(false);	// We should never hit this !!
else
{
if(var.P(j)==1)
nClauseCount += PrintSum1(fp, Svar, var.B(i), var.A(j-i+1), var.C(i, j-1));
else
_ASSERTE(false);	// P[n] should always be equal to 1

nClauseCount += PrintCarry0(fp, Svar, var.B(i), var.A(j-i+1), var.C(i, j-1));
}

return nClauseCount;
}  ```

The PrintCarry, PrintSum etc... are helper functions to output the CNF expressions for Sum, Carry values and their code can be found in the attached project. You need GMP Multiprecision library to build and test it.