Simplification de DNF, Subsumption

Bonjour à tous !

Je suis en train de développer un programme permettant de convertir une formule logique en DNF, et de préférence en une DNF la plus simple possible.

Une des simplifications possible est la subsumption

Code:

---

(A ou (A et B) = A

---

A vue de nez, le genre de données que je vais utiliser va vite me générer des clauses gigantesques mais dans lesquelles il y aura beaucoup de simplifications de ce genre à faire.

J'ai bossé sur l'algo général de ma conversion en DNF, c'est prêt, il me manque la détection et la simplifications des subsumption et la je planche.

J'aimerai éviter une comparaison 2 à 2 de toutes mes conjonctions, mais j'ai pas beaucoup d'idée sur comment faire autrement, donc si quelqu'un maitrise le sujet et peu me filer un coup de pouce, je lui en serait grandement reconnaissant ! ^^

Evidemment vu que j'ai replongé dans la logique il n'y a pas si longtemps, il y a de fortes chances que je soit pas claire du tout, si c'est le cas hésitez pas à le signaler.

Merci d'avance

Ca se fait à partir de ton arbre de syntaxe abstraite.

L'idée est de filtrer l'arbre à la recherche de motifs.

Par exemple en supposant que l'arbre est noté (Noeud, Fils1,Fils2,...) :
-> (Et,A,A) à remplacer par (A)
-> (Ou,A,A) à remplacer par (A)
-> (Et,A,Vrai) à remplacer par (A)
-> (Ou,A,Vrai) à remplacer par Vrai
-> ...

Et dans ton cas :
-> (Ou,A,(Et,A,B)) -> A remplacer par A

il y a des dizaines de motifs que tu peux filtrer.

Une méthode simple consiste à rechercher le motif et à l'appliquer. Tu arrêtes l'algo de simplification quand tu n'as pas pu effectuer de modif (c'est donc qu'au regard de tes motifs de simplification tu n'as plus rien à faire).