Horn-satisfiabilité

Une formule de Horn est une conjonction de clauses contenant chacune au plus un littéral positif, c'est-à-dire une conjonction de clauses de Horn.

Puisque le problème SAT est NP-complet, donc vérifiable en temps polynomial et plus difficile que tout problème dans NP, il est naturel de rechercher des problèmes proches mais plus "faciles" à résoudre. C'est notamment le cas de la satisfaisabilité d'une formule de Horn, puisqu'il s'agit d'un problème P-complet, plus difficile que tout problème dans P.

De plus, la satisfaisabilité d'une formule de Horn est décidable en temps linéaire en la taille de la formule.

Un algorithme naïf résout ce problème en temps $O(N^{2})$, en partant du principe qu'une formule de Horn contient trois types de clauses :

• des clauses de Horn strictes, de la forme $\lnot q_{1}\lor \lnot q_{2}\lor \dots \lor \lnot q_{n}\lor p$
• des clauses de Horn positives, de la forme $p$
• des clauses de Horn négatives, de la forme $\lnot q_{1}\lor \lnot q_{2}\lor \dots \lor \lnot q_{n}$

Puisqu'une formule de Horn ne contenant pas de clause de Horn positive est toujours satisfaisable (car il suffit d'affecter la valeur fausse à tous les littéraux pour satisfaire chaque clause), on cherche à éliminer toutes les clauses positives. On y arrive en affectant au littéral contenu dans chaque clause positive la valeur vraie, puis en propageant ces modifications, c'est-à-dire en supprimant les clauses positives ou strictes où notre littéral apparaît, et en effaçant sa négation de chaque clause stricte ou négative où il apparaît.

Ce procédé peut générer d'autres clauses de Horn positives et il est donc nécessaire de l'itérer.