Solucionador SAT polinómico Zhegalkin

Los sistemas polinómicos son herramientas fundamentales en la solución de problemas difíciles en ciencia e ingeniería como la robótica, el razonamiento automatizado, la inteligencia artificial y el procesamiento de señales. Del mismo modo, desde los inicios de la era digital, las variables booleanas han sido la base de las operaciones informáticas. De ahí que la aplicación de técnicas algebraicas comunes al álgebra booleana se utilice ahora como método para resolver complejos sistemas de ecuaciones booleanas que antes sólo se pretendían resolver utilizando técnicas de lógica booleana. El objetivo de este proyecto es demostrar que los polinomios de Zhegalkin (también conocidos como Forma Algebraica Normal - ANF) son una forma alternativa de representar funciones booleanas. Para probar la hipótesis, se desarrolló un solucionador SAT de Zhegalkin (ZPSAT). Los resultados obtenidos tras las pruebas concluyeron que ZPSAT puede resolver una conjunción de ecuaciones XOR de forma eficiente en términos de fiabilidad y tiempo de computación. La heurística utilizada para construir ZPSAT se basó principalmente en los conceptos utilizados por las fórmulas de Horn y un método de multiplicación rápida de dos polinomios ANF conocido como transformada de Mobius.