| Attributes | Values |
|---|
| rdfs:label
| - Horn-satisfiabilité (fr)
- Markierungsalgorithmus (de)
- Satisfatibilidade de Horn (pt)
|
| rdfs:comment
| - 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. Ce procédé peut générer d'autres clauses de Horn positives et il est donc nécessaire de l'itérer. (fr)
|
| sameAs
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| dbo:wikiPageWikiLink
| |
| page length (characters) of wiki page
| |
| dct:subject
| |
| prop-fr:wikiPageUsesTemplate
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| named after
| |
| has abstract
| - 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 , en partant du principe qu'une formule de Horn contient trois types de clauses :
* des clauses de Horn strictes, de la forme
* des clauses de Horn positives, de la forme
* des clauses de Horn négatives, de la forme 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. (fr)
|
| is dbo:wikiPageWikiLink
of | |
| is oa:hasTarget
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)