Convertir circuito sentó a 3-SAT

Question

Estoy tratando de convertir Entero de la Factorización de a $3-SAT$.

Hasta ahora me las arreglé para convertir a un Circuito de SAT, pero no sé cómo hacer el paso final.

Es de esta forma que buscar 3*3 la multiplicación:

• cierto = (1 $\wedge$ 3)
• falso = (2 $\wedge$ 3) $\oplus$ (1 $\wedge$ 4)
• falso = (2 $\wedge$ 4) $\oplus$ (2 $\wedge$ 3) $\wedge$ (1 $\wedge$ 4) $\wedge$ ((2 $\wedge$ 3) $\oplus$ (1 $\wedge$ 4))
• cierto = (2 $\wedge$ 4) $\vee$ (2 $\wedge$ 3) $\wedge$ (1 $\wedge$ 4) $\wedge$ ((2 $\wedge$ 3) $\oplus$ (1 $\wedge$ 4)) $\wedge$ (2 $\wedge$ 4)

Mi átomo de cálculo:

• $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

Tenemos:

$$\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}$$

En la cuenta de mi $C^{out}_{i,j}$ es diferente; esta es la fórmula que me sale en busca de la Serpiente Llena en un carry-save-multiplicación de matriz (de aquí):

Que se utiliza en el multiplicador de la unidad:

En la imagen de arriba, $m_j$ es nuestro $X_i$ $q_i$ es nuestro $Y_j$. Nuestra $P_{i,j}$ es la salida Y la puerta. El cable que viene de la parte superior es el $S^{out}$ de la unidad por encima de nosotros, es decir,. $S^{in}_{i,j}$. Esto es lo que el 4x4 MULT circuito se parece a:

Ahora, a pesar de que mi $C^{out}_{i,j}$ es diferente, puede ser equivalente. En cualquier caso, la metodología siguiente esquema de trabajo para ambos.

---

En el anidado de expresiones, para cada operación $(y \star z)$ donde $y,z$ son variables, y $\star$ es de alguna operación $\in \left\{\vee,\wedge,\oplus\right\}$, de crear una nueva variable, y reemplazar el $(y \star z)$ con la nueva variable. A continuación, utilizando las identidades, a continuación, agregar las cláusulas de la CNF, que entorpece la nueva variable sea igual a la sustituye expresión. Repita esto hasta que no hay operaciones de la izquierda.

Vamos a empezar con $P_{i,j}=X_i\wedge Y_j$:

Para 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\implica (y\wedge z)\right] &\ffi& \left[ \begin{array}{} \phantom{~\wedge~}(x\implies y)\\ {~\wedge~}(x\implies z) \end{array} \right]\\ &\ffi& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x\vee y)\\ {~\wedge~}(\neg x\vee z) \end{array} \right] &\tilde\\\hline\\ \left[(y\wedge z)\implica x\right] &\ffi& \left[ \neg x \implica \neg (y\wedge z) \right]\\ &\ffi& \left[ \neg x \implica (\neg y\v \neg z) \right]\\ &\ffi& \left[ ( x \v \neg y\v \neg z) \right] &\tilde\\\hline\\ \left[x=y\wedge z\right] &\ffi& \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] &\marca de verificación \end{array}$$

Así, podemos agregar $(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)$ a la CNF.

A continuación, vamos a convertir este: $S^{out}_{i,j}=(S^{in}_{i,j} \oplus P_{i,j}) \oplus C^{in}_{i,j}$.

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

A continuación,$S^{out}_{i,j}=\alpha_{i,j} \oplus C^{in}_{i,j}$.

Para general $x = y \oplus z$:

$$\requieren{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 \implica y\oplus z) &\ffi& \left[ \begin{array}{} \phantom{~\wedge~}(x \implies y\vee z)\\ {~\wedge~}(x \implies \neg y\vee \neg z)\\ \end{array} \right] \\ &\ffi& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x \vee y\vee z)\\ {~\wedge~}(\neg x \vee \neg y\vee \neg z)\\ \end{array} \right] &\marca de verificación \\\hline\\ (y\oplus z\implica x) &\ffi& \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] \\ &\ffi& \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] &\marca de verificación \\ &\ffi& \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] &\marca de verificación \\\hline\\ (x = y\oplus z) &\ffi& \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] &\marca de verificación \\ &\ffi& \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] &\marca de verificación \\ \end{array}$$

Averiguar qué cláusulas para agregar ahora, de una vez por $\alpha_{i,j}$ (una nueva variable) y de una vez por $S^{out}_{i,j}$, para un total de $8$ cláusulas.

Finalmente, para $C^{out}_{i,j}$, usted puede reducir el funcionamiento interno, y reemplazarlos con las variables. El único resto de la operación yo no te enseñan a reemplazar es $(y \vee z)$. Así, por $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 \implica y\vee z) &\ffi& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x \vee y\vee z)\\ \end{array} \right] &\marca de verificación \\\hline\\ (y\vee z \implica x) &\ffi& \left[ \begin{array}{} \phantom{~\wedge~}(y \implies x)\\ {~\wedge~}(z \implies x)\\ \end{array} \right] \\ &\ffi& \left[ \begin{array}{} \phantom{~\wedge~}(\neg y \vee x)\\ {~\wedge~}(\neg z \vee x)\\ \end{array} \right] &\marca de verificación \\\hline\\ (x=y\vee z) &\ffi& \left[ \begin{array}{} \phantom{~\wedge~}(\neg x \vee y\vee z)\\ \\\\ {~\wedge~}(\neg y \vee x)\\ {~\wedge~}(\neg z \vee x)\\ \end{array} \right] &\marca de verificación \end{array}$$

Así que ahora vamos a resolver el final, $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}$$

Por lo tanto, tenemos $\alpha_{i,j}=S^{in}_{i,j}\oplus P_{i,j}$. A continuación, establezca $\beta_{i,j}=S^{in}_{i,j}\wedge P_{i,j}$ (utilizando el $\wedge$ operación de la anterior). Siguiente, reemplazar las variables de la fórmula:

$$\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}$$

Ahora usted puede codificar $C^{out}_{i,j}=\gamma_{i,j} \vee \beta_{i,j}$ $\vee$ operación de conversión. Y no te olvides de codificar todas las nuevas variables, $\alpha_{i,j},\beta_{i,j},\gamma_{i,j}$ con sus respectivas operaciones.

Answer 2

Que las puertas tienen en sus circuitos? Suponiendo que usted tiene sólo compuertas NAND:

Asignar una variable proposicional para representar cada uno de los cables en el circuito. Entonces cada vez que hay una puerta NAND con entradas de $a$ $b$ y de salida $c$, tome las siguientes cláusulas: $$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)~)$$ Cada una de las cláusulas previene $c$ de tener el mal que el valor de una de las líneas en la tabla de verdad para la NAND, lo que obliga a tener el derecho de valor en ese caso.

Si usted tiene otras puertas de la NAND, reducir a la NAND circuitos primera, o crear las cláusulas de su tabla de verdad de una manera similar a la de arriba.

Por último, si $s$ es el alambre de salida, añadir la cláusula $$s \lor s \lor s$$