Solveur SAT de polynômes de Zhegalkin

Les systèmes polynomiaux sont des outils fondamentaux pour la résolution de problèmes difficiles en science et en ingénierie, tels que la robotique, le raisonnement automatique, l'intelligence artificielle et le traitement des signaux. De même, dès les premiers jours de l'ère numérique, les variables booléennes ont été à la base des opérations informatiques. Par conséquent, l'application de techniques algébriques courantes à l'algèbre de Boole est désormais utilisée comme méthode pour résoudre des systèmes d'équations booléennes complexes qui, auparavant, ne pouvaient être résolus qu'à l'aide de techniques de logique booléenne. L'objectif de ce projet est de démontrer que les polynômes de Zhegalkin (également connus sous le nom d'Algebraic Normal Form - ANF) sont une autre façon de représenter les fonctions booléennes. Afin de tester l'hypothèse, un résolveur SAT de Zhegalkin (ZPSAT) a été développé. Les résultats obtenus après les tests ont conclu que ZPSAT peut résoudre une conjonction d'équations XOR de manière efficace en termes de fiabilité et de temps de calcul. L'heuristique utilisée pour construire ZPSAT était principalement basée sur les concepts utilisés par les formules de Horn et une méthode de multiplication rapide de deux polynômes ANF connue sous le nom de transformation de Mobius.