Résolution d'un système d'équation logiques

[sourivore]

Bonjour,

Essayant de développer un algorithme de résolution d'un jeu de logique, je suis confronté au problème suivant :
J'ai une équation logique sur 9 variables formée exclusivement de ET et de XOR, du genre :
(A1 ET A2 ET A3) XOR (B1 et B2 et B3) XOR (C1 et C2 et C3)
Ceci n'est qu'un exemple car normalement il n'y a qu'une solution (par exemple A1 = A3 = C2 = true et le reste est false)

Y a t il un moyen de résoudre cette équation sans avoir à passer par un tableau de Karnaugh ou une table de vérité, ce qui impliquerait d'avoir à calculer les 2 puissance 9 combinaisons possibles, cas qui serait encore pire si je suis sur un problème 4x4 => 2 puissance 16 combinaisons) ?

N'y a t il pas moyen de le réduire à un calcul matriciel par exemple ?

Je vous donne un exemple concret afin de pouvoir tester l'algo :

((A1 et A3) xor (A1 et B2) xor (B2 et A3)) et (A1 xor B2 xor C1) et (A3 xor B2 xor C3) et !B1 et !B3 et !A2 et !C2

Résultat =
A1 = A3 = true, le reste à false

Ce qui est équivalent à dire que cette équation logique se réduit sous sa forme la plus simple à :
A1 et !A2 et A3 et !B1 et !B2 et !B3 et !C1 et !C2 et !C3

Merci d'avance au génie qui aura une idée

[Aleph69]

Bonjour,

il existe des algorithmes de factorisation pour simplifier les expressions logiques et ainsi réduire la complexité de l'évaluation des tables de vérité. A part cette approche, je ne vois rien d'autre à faire.

[Zavonen]

Peut-être passer en forme normale conjonctive pour scinder l'équation en un système.

[sourivore]

Merci pour vos réponses.

En effet, il faudrait utiliser un algorithme de simplification afin de passer en une formule normale conjonctive simple (uniquement des "ET"), ce qui me donnerait ma solution unique.

Mais je ne trouve pas d'algorithme qui ne passerait pas par une table de Karnaugh (contrairement à Quin Mc Cluskey par exemple) car ceci conduirait à calculer toutes les possibilités, ce qui est assez imposant.

Merci d'avance si vous avez plus d'infos

[Zavonen]

Demande à l'ami google avec 'algorithme forme normale conjonctive' beaucoup de réponses pertinentes, soit en langage clair soit en caml