In formal logic, Horn-satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable or not. Horn-satisfiability and Horn clauses are named after Alfred Horn.
Attributes | Values |
---|
rdf:type
| |
rdfs:label
| - Horn-satisfiability (en)
- Horn-satisfiabilité (fr)
- Satisfatibilidade de Horn (pt)
|
rdfs:comment
| - In formal logic, Horn-satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable or not. Horn-satisfiability and Horn clauses are named after Alfred Horn. (en)
- 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)
- Na lógica formal, Satisfatibilidade de Horn, ou HORNSAT, é o problema de decidir se um dado conjunto de cláusulas de Horn é satisfatível ou não. Uma cláusula de Horn é uma cláusula com no máximo um literal positivo, chamado cabeça da cláusula, e qualquer número de literais negativos, formando o corpo da cláusula. Uma fórmula de Horn é uma fórmula proposicional formada pela conjunção de cláusulas de Horn.O problema da satisfatibilidade de Horn é solucionável em tempo linear. Um algoritmo de tempo polinomial para satisfatibilidade de Horn é baseado na regra de propagação de unidade: se a fórmula contém uma cláusula composta de um único literal (uma cláusula unitária), então todas as cláusulas que contenham (exceto ela mesma) são removidas, e todas as cláusulas contendo tem esse literal r (pt)
|
dcterms:subject
| |
Wikipage page ID
| |
Wikipage revision ID
| |
Link from a Wikipage to another Wikipage
| |
sameAs
| |
dbp:wikiPageUsesTemplate
| |
has abstract
| - In formal logic, Horn-satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable or not. Horn-satisfiability and Horn clauses are named after Alfred Horn. (en)
- 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)
- Na lógica formal, Satisfatibilidade de Horn, ou HORNSAT, é o problema de decidir se um dado conjunto de cláusulas de Horn é satisfatível ou não. Uma cláusula de Horn é uma cláusula com no máximo um literal positivo, chamado cabeça da cláusula, e qualquer número de literais negativos, formando o corpo da cláusula. Uma fórmula de Horn é uma fórmula proposicional formada pela conjunção de cláusulas de Horn.O problema da satisfatibilidade de Horn é solucionável em tempo linear. Um algoritmo de tempo polinomial para satisfatibilidade de Horn é baseado na regra de propagação de unidade: se a fórmula contém uma cláusula composta de um único literal (uma cláusula unitária), então todas as cláusulas que contenham (exceto ela mesma) são removidas, e todas as cláusulas contendo tem esse literal removido. O resultado da segunda regra pode gerar uma outra cláusula unitária, a qual será propagada da mesma maneira. Se não existem cláusulas unitárias, a fórmula pode ser satisfeita simplesmente pela atribuição de valoração negativa às variáveis restantes. A fórmula é insatisfatível se essa transformação gera um par de cláusulas unitárias opostas e . Satisfatibilidade de Horn é, na verdade, um dos problemas mais "difíceis" ou "mais expressivos" que se sabe ser computável em tempo polinomial, no sentido de que é um problema P-completo. Esse algoritmo também permite a determinação de uma valoração-verdade de formulas de Horn satisfatíveis: a todas as variáveis contidas em uma cláusula unitária é atribuído o valor que satisfaça a cláusula unitária em questão; a todos os outros literais é atribuída valoração negativa. A atribuição resultante é o modelo mínimo da fórmula de Horn, isto é, a atribuição ter um conjunto mínimo de variáveis cujo valor-verdade é positivo, onde a comparação é feita usando set containment. Usar um algoritmo linear para propagação de unidade faz com que o algoritmo seja linear no tamanho da fórmula. Uma generalização da classe das fórmulas de Horn é a das fórmulas renomeáveis de Horn (renameble-Horn formulae), que é o conjunto de fórmulas que podem ser passadas para a forma de Horn através da substituição de algumas variáveis por suas respectivas negações. Conferir a existência de tal substituição pode ser feito em tempo linear; portanto a satisfatibilidade de tais fórmulas está em P, já que pode ser solucionada realizando essa substituição e, em seguida, checando a satisfatibilidade da fórmula de Horn resultante. O problema da satisfatibilidade de Horn também pode ser requerido para (propositional many-valued logics). Os algoritmos não são geralmente lineares, mas alguns são polinomiais; ver Hähnle (2001 ou 2003) para uma pesquisa. (pt)
|
prov:wasDerivedFrom
| |
page length (characters) of wiki page
| |
foaf:isPrimaryTopicOf
| |
is Link from a Wikipage to another Wikipage
of | |
is Wikipage redirect
of | |
is foaf:primaryTopic
of | |