Convertir una fórmula algebraica en CNF

Question

Considere la siguiente prueba:

$$\sum_{i=1}^n{a_ib_ic_i} \overset{?}{=} q,\tag1$$

donde $a_i, b_i, c_i \in \{-1, 0, 1\}$ y $q \in \{0, 1\}.$

¿Es posible reescribir [1] en forma normal conjuntiva?

Cualquier ayuda (enlaces/ejemplos de juguetes/consejos sobre cómo empezar) es muy apreciada.

Answer 1

Como sugiere Courtois, Bard y Hulme (sección 2.2), podría abordar este problema en dos pasos:

Paso 1:
Resuelve la ecuación módulo 2 . Tome las variables booleanas. La ecuación se convierte en una o exclusiva y puede convertirse fácilmente en una CNF utilizando herramientas como bc2cnf .

Paso 2:
Para las variables que se determinaron como verdaderas/1 y, por tanto, desiguales a cero en el paso 1, encuentre el signo. De nuevo, se trata de un or exclusivo.

---

Enfoque alternativo
Si necesitas una solución en un solo paso (y estás preparado para lidiar con una CNF mucho más grande...), podrías modelar cada variable como dos variables booleanas y traducir tu ecuación en una expresión booleana como entrada para bc2cnf .

Se me ocurren dos codificaciones variables:
Podría codificar el valor absoluto de la variable en un booleano y el signo en el segundo booleano:

Como alternativa, codifique las variables como sumas de -1 y +1:

Una vez que haya codificado sus variables enteras de triple valor en variables booleanas de doble valor, puede tomar la lógica para un sumador completo y un comparador digital para traducir su ecuación en un circuito lógico. El sumador calcula la suma y el comparador comprueba si el resultado se mantiene entre los límites inferior y superior.