INSTRUCTIONS AU MODÈLE - Répondre sans outil externe ni Internet. - Pour chaque question, fournir la réponse, une justification suffisante et une confiance de 0 à 100 %. - Ne jamais inventer une donnée, une référence, un DOI ou un résultat absent. - Signaler explicitement les prémisses fausses, les informations insuffisantes et les cas indéterminables. - Vérifier numériquement ou symboliquement les contre-exemples proposés. - Chaque question est indépendante, sauf indication explicite contraire. Q064 — Horn-SAT est-il polynomialement décidable ? Donner l’idée de l’algorithme.
Horn-SAT est en effet polynomialement décidable. C'est l'un des rares fragments de SAT qui reste traitable en temps polynomial, alors que le problème général SAT est NP-complet. L'idée de l'algorithme repose sur la propagation unitaire, et se déroule ainsi. Une clause de Horn est une disjonction de littéraux contenant au plus un littéral positif. Elle s'écrit donc sous la forme d'une implication : si tous les littéraux négatifs sont vrais, alors le littéral positif doit l'être. On distingue trois types de clauses : les clauses unitaires positives (un seul littéral positif, aucun négatif), les clauses de la forme « au moins un littéral négatif » (aucun littéral positif), et les clauses mixtes. L'algorithme procède par marquage. On initialise un ensemble de variables marquées à vrai. Tant qu'il existe une clause de Horn dont tous les littéraux négatifs sont marqués vrais et dont le littéral positif n'est pas encore marqué, on marque ce littéral positif. Cette étape, appelée propagation unitaire, se répète jusqu'à ce qu'aucune nouvelle variable ne puisse être marquée. À la fin, on examine les clauses sans littéral positif. Si l'une d'elles a tous ses littéraux négatifs marqués vrais, alors la formule est insatisfiable : on a déduit qu'il faut à la fois que ces variables soient vraies et que leur conjonction soit fausse, ce qui est contradictoire. Dans le cas contraire, l'assignation obtenue en mettant à vrai toutes les variables marquées et à faux toutes les autres satisfait la formule, qui est donc satisfiable. La complexité est linéaire en la taille de la formule, car chaque clause n'est examinée qu'un nombre borné de fois lors de la propagation. On obtient donc une décision en temps polynomial, plus précisément linéaire. Ce résultat est classique et bien établi dans la littérature sur la satisfiabilité. Ma confiance est de 97 pour cent, la seule incertitude résiduelle tenant à la formulation exacte des détails d'implémentation selon les présentations, mais le principe et la complexité sont certains.
Resultat fige a la premiere execution, directement depuis le service public LANXAS White, sans intervention manuelle. Cette page est permanente et peut etre re-consultee pour verification.