Convert Circuit SAT to 3-SAT

Question

I am trying to convert Integer Factorization to $3-SAT$.

So far I managed to convert it to Circuit SAT, but I don't know how to make the final step.

This is how it look for 3*3 multiplication:

• true = (1 $\wedge$ 3)
• false = (2 $\wedge$ 3) $\oplus$ (1 $\wedge$ 4)
• false = (2 $\wedge$ 4) $\oplus$ (2 $\wedge$ 3) $\wedge$ (1 $\wedge$ 4) $\wedge$ ((2 $\wedge$ 3) $\oplus$ (1 $\wedge$ 4))
• true = (2 $\wedge$ 4) $\vee$ (2 $\wedge$ 3) $\wedge$ (1 $\wedge$ 4) $\wedge$ ((2 $\wedge$ 3) $\oplus$ (1 $\wedge$ 4)) $\wedge$ (2 $\wedge$ 4)

My atom calculation:

• $p$ = XY
• $Sum_{out}$ = ($Sum_{in}$ $\oplus$ $p$) $\oplus$ $Carry_{in}$
• $Carry_{out}$= (($Sum_{in}$ $\wedge$ $p$) $\vee$ $Carry_{in}$) $\wedge$ ($Sum_{in}$ $\oplus$ $p$);

Answer 1

We have:

$$ \begin{eqnarray} P_{i,j}&=&X_i\wedge Y_j\\ S^{out}_{i,j}&=&(S^{in}_{i,j} \oplus P_{i,j}) \oplus C^{in}_{i,j}\\ %C^{out}_{i,j}&=& (C^{in}_{i,j} \wedge (A\oplus B) ) \vee (A\wedge B)\\ C^{out}_{i,j}&=& (C^{in}_{i,j} \wedge (S^{in}_{i,j}\oplus P_{i,j}) ) \vee (S^{in}_{i,j}\wedge P_{i,j})\\ \end{eqnarray} $$

Notice my $C^{out}_{i,j}$ is different; this is the formula I get from looking at the Full Adder in a carry-save-multiplication-array (from here):

Which is used in the multiplier-unit:

In the above image, $m_j$ is our $X_i$ and $q_i$ is our $Y_j$. Our $P_{i,j}$ is the output of that AND-gate. The wire coming in from the top is the $S^{out}$ of the unit above us, ie. $S^{in}_{i,j}$. This is what the 4x4 MULT circuit looks like:

Now, even though my $C^{out}_{i,j}$ is different, they may still be equivalent. In any case, the methodology I outline below will work for both.

---

In the nested expressions, for each operation $(y \star z)$, where $y,z$ are variables, and $\star$ is some operation $\in \left\{\vee,\wedge,\oplus\right\}$, you create a new variable, and replace the $(y \star z)$ with the new variable. Then using the identities below, you add clauses to the CNF, constraining the new variable to be equal to the replaced expression. Repeat this until there are no operations left.

Let's start with $P_{i,j}=X_i\wedge Y_j$:

For general $x = y \wedge z$:

$$ \begin{array}{ccl|c} %\mathbf{\text{Statement}}&&%&\mathbf{\text{#}}&\mathbf{\text{Reason}} \\ &&&\mathbf{\genfrac{}{}{0}{1}{\text{Clause}}{\text{format}}}\\\hline\\ \left[x=y\wedge z\right] &\iff& \left[x\iff y\wedge z\right]\\ &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(x\implies y\wedge z)\\ ~\wedge~(y\wedge z\implies x) \end{array} \right] \\\hline\\ \left[x\implies (y\wedge z)\right] &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(x\implies y)\\ {~\wedge~}(x\implies z) \end{array} \right]\\ &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x\vee y)\\ {~\wedge~}(\neg x\vee z) \end{array} \right] &\checkmark\\\hline\\ \left[(y\wedge z)\implies x\right] &\iff& \left[ \neg x \implies \neg (y\wedge z) \right]\\ &\iff& \left[ \neg x \implies (\neg y\vee \neg z) \right]\\ &\iff& \left[ ( x \vee \neg y\vee \neg z) \right] &\checkmark\\\hline\\ \left[x=y\wedge z\right] &\iff& \left[\begin{array}{} \phantom{~\wedge~}( x \vee \neg y\vee \neg z)\\ \\\\ {~\wedge~}(\neg x\vee y)\\ {~\wedge~}(\neg x\vee z)\end{array}\right] &\checkmark \end{array} $$

So, we can add $(P_{i,j}\vee \neg X_i \vee \neg Y_j) \wedge (\neg P_{i,j} \vee X_i) \wedge (\neg P_{i,j} \vee Y_j)$ to the CNF.

Then let's convert this one: $S^{out}_{i,j}=(S^{in}_{i,j} \oplus P_{i,j}) \oplus C^{in}_{i,j}$.

Let $\alpha_{i,j}=S^{in}_{i,j} \oplus P_{i,j}$.

Then $S^{out}_{i,j}=\alpha_{i,j} \oplus C^{in}_{i,j}$.

For general $x = y \oplus z$:

$$\require{cancel} \begin{array}{ccl|c} \\ &&&\mathbf{\genfrac{}{}{0}{1}{\text{Clause}}{\text{format}}}\\\hline\\ (x = y\oplus z) &\iff& (x \iff y\oplus z) \\ &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(x \implies y\oplus z)\\ {~\wedge~}(y\oplus z \implies x)\\ \end{array} \right] \\\hline\\ (x \implies y\oplus z) &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(x \implies y\vee z)\\ {~\wedge~}(x \implies \neg y\vee \neg z)\\ \end{array} \right] \\ &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x \vee y\vee z)\\ {~\wedge~}(\neg x \vee \neg y\vee \neg z)\\ \end{array} \right] &\checkmark \\\hline\\ (y\oplus z\implies x) &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(y \wedge z \implies \neg x)\\ {~\wedge~}(y \wedge \neg z \implies x)\\ {~\wedge~}(\neg y \wedge z \implies x)\\ {~\wedge~}(\neg y \wedge \neg z \implies \neg x)\\ \end{array} \right] \\ &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(\neg y \vee \neg z \vee \neg x)\\ {~\wedge~}(\neg y \vee z \vee x)\\ {~\wedge~}(y \vee \neg z \vee x)\\ {~\wedge~}(y \vee z \vee \neg x)\\ \end{array} \right] &\checkmark \\ &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x \vee \neg y \vee \neg z)\\ {~\wedge~}(x \vee \neg y \vee z)\\ {~\wedge~}(x \vee y \vee \neg z)\\ {~\wedge~}( \neg x \vee y \vee z)\\ \end{array} \right] &\checkmark \\\hline\\ (x = y\oplus z) &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x \vee y\vee z)\\ {~\wedge~}(\neg x \vee \neg y\vee \neg z)\\ \\\\\\ \cancel{{~\wedge~}(\neg x \vee \neg y \vee \neg z)}\\ {~\wedge~}(x \vee \neg y \vee z)\\ {~\wedge~}(x \vee y \vee \neg z)\\ \cancel{{~\wedge~}( \neg x \vee y \vee z)}\\ \end{array} \right] &\checkmark \\ &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x \vee y\vee z)\\ {~\wedge~}(\neg x \vee \neg y\vee \neg z)\\ {~\wedge~}(x \vee \neg y \vee z)\\ {~\wedge~}(x \vee y \vee \neg z)\\ \end{array} \right] &\checkmark \\ \end{array} $$

Figure out which clauses to add now, once for $\alpha_{i,j}$ (a new variable) and once for $S^{out}_{i,j}$, for a total of $8$ clauses.

Finally, for $C^{out}_{i,j}$, you can reduce the inner operations, and replace them with variables. The only remaining operation I didn't teach you to replace is $(y \vee z)$. So for $x=y\vee z$:

$$ \begin{array}{ccl|c} \\ &&&\mathbf{\genfrac{}{}{0}{1}{\text{Clause}}{\text{format}}}\\\hline\\ (x=y\vee z) &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(x \implies y\vee z)\\ {~\wedge~}(y\vee z \implies x)\\ \end{array} \right] \\\hline\\ (x \implies y\vee z) &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x \vee y\vee z)\\ \end{array} \right] &\checkmark \\\hline\\ (y\vee z \implies x) &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(y \implies x)\\ {~\wedge~}(z \implies x)\\ \end{array} \right] \\ &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(\neg y \vee x)\\ {~\wedge~}(\neg z \vee x)\\ \end{array} \right] &\checkmark \\\hline\\ (x=y\vee z) &\iff& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x \vee y\vee z)\\ \\\\ {~\wedge~}(\neg y \vee x)\\ {~\wedge~}(\neg z \vee x)\\ \end{array} \right] &\checkmark \end{array} $$

So now let's solve the final one, $C^{out}$:

$$ \begin{eqnarray} C^{out}_{i,j}&=& (C^{in}_{i,j} \wedge (S^{in}_{i,j}\oplus P_{i,j}) ) \vee (S^{in}_{i,j}\wedge P_{i,j}) \end{eqnarray} $$

So, we have $\alpha_{i,j}=S^{in}_{i,j}\oplus P_{i,j}$. Next, set $\beta_{i,j}=S^{in}_{i,j}\wedge P_{i,j}$ (using the $\wedge$ operation from above). Next, replace variables in the formula:

$$ \begin{eqnarray} C^{out}_{i,j} &=& (C^{in}_{i,j} \wedge (S^{in}_{i,j}\oplus P_{i,j}) ) \vee (S^{in}_{i,j}\wedge P_{i,j}) \\ &=& (C^{in}_{i,j} \wedge \alpha_{i,j}) \vee (\beta_{i,j})\\ \gamma_{i,j} &=& C^{in}_{i,j} \wedge \alpha_{i,j}\\ C^{out}_{i,j} &=& \gamma_{i,j} \vee \beta_{i,j} \end{eqnarray} $$

Now you can encode $C^{out}_{i,j}=\gamma_{i,j} \vee \beta_{i,j}$ with the $\vee$ operation conversion. And don't forget to encode the all the new variables, $\alpha_{i,j},\beta_{i,j},\gamma_{i,j}$ with their respective operations.

Answer 2

Which gates do you have in your circuits? Supposing you have only NAND gates:

Assign a propositional variable to represent each wire in the circuit. Then whenever there's a NAND gate with inputs $a$ and $b$ and output $c$, take the following clauses: $$ a \lor b \lor c \qquad (\iff \neg(\bar a \land \bar b \land \bar c)~)$$ $$ \bar a \lor b \lor c \qquad (\iff \neg(a \land \bar b \land \bar c)~) $$ $$ a \lor \bar b \lor c \qquad (\iff \neg(\bar a \land b \land \bar c)~) $$ $$ \bar a \lor \bar b \lor \bar c \qquad (\iff \neg(a \land b \land c)~) $$ Each of the clauses prevents $c$ from having the wrong value for one of the lines in the truth table for NAND, thereby forcing it to have the right value in that case.

If you have gates other than NAND, either reduce to NAND circuits first, or create clauses from their truth table in a similar way to the above one.

Finally if $s$ is the output wire, add the clause $$ s \lor s \lor s $$