DPLL algorithm (original) (raw)
En informatique, l'algorithme de Davis–Putnam–Logemann–Loveland (DPLL) est un algorithme de backtracking, complet, de résolution du problème SAT. Le problème SAT est un problème important à la fois d'un point de vue théorique, en particulier en théorie de la complexité où il est le premier problème prouvé NP-complet et pratique puisqu'il peut apparaître lors de la résolution de problèmes de planification classique, model checking, ou encore diagnostic et jusqu'au configurateur d'un PC ou de son système d'exploitation[réf. nécessaire].
| Property | Value |
|---|---|
| dbo:abstract | In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem. It was introduced in 1961 by Martin Davis, George Logemann and Donald W. Loveland and is a refinement of the earlier Davis–Putnam algorithm, which is a resolution-based procedure developed by Davis and Hilary Putnam in 1960. Especially in older publications, the Davis–Logemann–Loveland algorithm is often referred to as the "Davis–Putnam method" or the "DP algorithm". Other common names that maintain the distinction are DLL and DPLL. (en) El algoritmo DPLL/Davis-Putnam-Logemann-Loveland es un algoritmo completo basado en la vuelta atrás que sirve para decidir la satisfactibilidad de las fórmulas de lógica proposicional en una forma normal conjuntiva, es decir, para resolver el problema . Fue presentado en 1962 por Martin Davis, Hilary Putnam, y y es una refinación del previo algoritmo de Davis-Putnam, el cual es un procedimiento de resolución desarrollado por Davis y Putnam en 1960. El algoritmo Davis-Putnam-Logemann-Loveland es nombrado a menudo como el "método Davis-Putnam" o el "algoritmo DP", especialmente en publicaciones antiguas. Otros nombres comunes que mantienen la distinción son DLL y DPLL. El DPLL es un procedimiento muy eficiente y tras más de 40 años aún conforma la base de los solucionadores más eficaces de SAT, así como de muchos demostradores de teoremas para fragmentos de lógica de primer orden. (es) En informatique, l'algorithme de Davis–Putnam–Logemann–Loveland (DPLL) est un algorithme de backtracking, complet, de résolution du problème SAT. Le problème SAT est un problème important à la fois d'un point de vue théorique, en particulier en théorie de la complexité où il est le premier problème prouvé NP-complet et pratique puisqu'il peut apparaître lors de la résolution de problèmes de planification classique, model checking, ou encore diagnostic et jusqu'au configurateur d'un PC ou de son système d'exploitation[réf. nécessaire]. (fr) Het DPLL-algoritme (Davis-Putnam-Logemann-Loveland algoritme) is een algoritme voor het onderzoeken van de vervulbaarheid van een propositie in conjunctieve normaalvorm (dit probleem is ook bekend als CNF-SAT). Het algoritme werd gepubliceerd in 1962 door , Hilary Putnam, en als een verbetering van een eerder algoritme van Davis en Putnam uit 1960. Het algoritme maakt gebruik van backtracking indien nodig. Er bestaan allerlei verbeterde varianten van het DPLL-algoritme, zoals het , en . (nl) DPLL (Davis-Putnam-Logemann-Loveland) è un algoritmo di ricerca esaustiva, basato sul backtracking, utilizzato per decidere la soddisfacibilità booleana di formule di logica proposizionale in forma normale congiuntiva (CNF), problema noto come . È stato introdotto nel 1962 da Martin Davis, Hilary Putnam, e , e rappresenta una specializzazione del precedente algoritmo di Davis-Putnam, una procedura sviluppata nel 1960. Per questo, soprattutto nelle pubblicazioni più vecchie l'algoritmo Davis-Logemann-Loveland è spesso indicato come il "metodo Davis-Putnam" o "algoritmo DP". Altre nomenclature comuni che mantengono la distinzione fra i due sono DLL e DPLL. Il DPLL è una procedura assai efficiente, e dopo più di 40 anni forma ancora la base dei più efficienti risolutori SAT completi, così come per molti dimostratori di teoremi per frammenti di logica del primo ordine. (it) Davis-Putnam-Logemann-Lovelandアルゴリズム（DPLLアルゴリズム、英: Davis-Putnam-Logemann-Loveland algorithm）とは、数理論理学および計算機科学において、論理式の充足可能性を調べるアルゴリズムである。連言標準形で表現された命題論理式を対象とし、論理式を真（True）にできるかどうかを判定する。この判定問題はCNF-SATと呼ばれる。 このアルゴリズムは、1960年に発表されたデービス・パトナムのアルゴリズム（英: Davis–Putnam algorithm）の改良版として、1962年に（英語: Martin Davis）、（英語: George Logemann）、（英語: Donald W. Loveland）が発表した。 なお、文献によってはDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。 (ja) DPLL (алгоритм Дэвиса — Патнема — Логемана — Лавленда) — полный алгоритм поиска с возвратом для решения задачи CNF-SAT — определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме. Опубликован в 1962 году Мартином Дэвисом, Хилари Патнэмом, и как усовершенствование более раннего алгоритма Дэвиса — Патнема, основанного на правиле резолюций. Является высокоэффективным алгоритмом и спустя полвека сохраняет актуальность и используется в большинстве решателей для SAT и системах автоматического доказательства для фрагментов логики первого порядка. (ru) O algoritmo DPLL/Davis-Putnam-Logemann-Loveland é um algoritmo completo baseado em backtracking (re-leitura ou voltar atrás) para decidir a satisfatibilidade das fórmulas de lógica proposicional na forma normal clausal, isto é, para solucionar o problema SAT. O algoritmo foi introduzido em 1962 por Martin Davis, Hilary Putnam, George Logemann e , sendo um refinamento do algoritmo de Davis-Putnam mais antigo, o qual é baseado num processo de resolução desenvolvido por Davis e Putnam em 1960. Principalmente em publicações antigas, o algoritmo de Davis-Logemann-Loveland é freqüentemente referenciado como “O Método Davis-Putnam” ou o “Algoritmo DP”. Outros nomes comuns que mantém a distinção são DLL e DPLL. DPLL é um procedimento altamente eficiente, e forma a base para os mais eficientes solucionadores SAT e outros problemas NP-completos que podem ser reduzidos para o problema SAT, e também para muitos para os fragmentos da lógica de primeira ordem. (pt) DPLL（Davis-Putnam-Logemann-Loveland）算法，是一種完備的、以回溯為基礎的算法，用於解決在合取範式（CNF）中命題邏輯的布爾可滿足性問題；也就是解決CNF-SAT问题。 它在1962年由馬丁·戴維斯、希拉里·普特南、和共同提出，作为早期的一种改进。戴維斯-普特南算法是戴維斯与普特南在1960年发展的一种算法。 DPLL是一种高效的程序，并且经过40多年还是最有效的SAT解法，以及很多一阶逻辑的自动定理证明的基础。 (zh) Алгоритм Девіса-Патнема-Логемана-Лавленд — це повний алгоритм пошуку з поверненням для визначення здійсненності булевих формул, записаних в кон'юнктивній нормальній формі (КНФ) для вирішення завдання CNF-SAT. Алгоритм був опублікований в 1962 році Мартіном Девісом, Гіларі Патнемом, Джорджем Логеманом й Дональдом Лавленд та представляє собою удосконалення більш раннього алгоритму Девіса-Патнема, методу, заснованого на правилі резолюцій, розробленого Девісом та Патнемом в 1960 році. DPLL — високо-ефективний алгоритм якому вже 50 років але все ще лежить в основі більшості ефективних вирішувачів для SAT, а також для систем автоматичного доведення теорем та фрагментів логіки першого порядку. (uk) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Dpll11.png?width=300 |
| dbo:wikiPageExternalLink | https://archive.org/details/machineprogramfo00davi http://portal.acm.org/citation.cfm%3Fcoll=GUIDE&dl=GUIDE&id=321034 |
| dbo:wikiPageID | 2745094 (xsd:integer) |
| dbo:wikiPageLength | 14433 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1094417709 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Proof_complexity dbr:Binary_tree dbc:Automated_theorem_proving dbr:Resolution_(logic) dbr:DPLL(T) dbr:Davis–Putnam_algorithm dbr:George_Logemann dbr:Model_checking dbr:NP-complete dbr:Conjunctive_normal_form dbr:Logic dbr:Communications_of_the_ACM dbr:Completeness_(logic) dbr:Computational_complexity_theory dbr:Computer_science dbr:Propositional_logic dbr:Automated_theorem_proving dbc:Articles_with_example_pseudocode dbr:Truth_value dbr:GRASP_(SAT_solver) dbr:First-order_logic dbr:Diagnosis_(artificial_intelligence) dbr:Journal_of_the_ACM dbr:Hilary_Putnam dbr:Backjumping dbr:Backtracking dbc:Constraint_programming dbr:Binary_decision_diagram dbr:Herbrandization dbr:Donald_W._Loveland dbr:Automated_planning_and_scheduling dbr:Martin_Davis_(mathematician) dbr:Boolean_satisfiability_problem dbc:SAT_solvers dbr:Search_algorithm dbr:Mathematical_theory dbr:SAT_solver dbr:Satisfiability_modulo_theories dbr:Conflict-Driven_Clause_Learning dbr:Implication_graph dbr:Propositional_variable dbr:Unit_propagation dbr:Polarity_(mathematical_logic) dbr:ZChaff dbr:Heuristic_function dbr:Short-circuiting_operator dbr:Stålmarck's_method |
| dbp:caption | After 5 fruitless attempts ', choosing the variable assignment a=1, b=1 leads, after unit propagation ', to success : the top left CNF formula is satisfiable. (en) |
| dbp:class | dbr:Boolean_satisfiability_problem |
| dbp:data | dbr:Binary_tree |
| dbp:imageSize | 300 (xsd:integer) |
| dbp:name | DPLL (en) |
| dbp:space | (en) |
| dbp:wikiPageUsesTemplate | dbt:Cite_book dbt:Cite_journal dbt:Commons_category dbt:Reflist dbt:Infobox_algorithm dbt:Algorithm-begin dbt:Algorithm-end |
| dcterms:subject | dbc:Automated_theorem_proving dbc:Articles_with_example_pseudocode dbc:Constraint_programming dbc:SAT_solvers |
| rdf:type | yago:Abstraction100002137 yago:Act100030358 yago:Activity100407535 yago:Algorithm105847438 yago:Event100029378 yago:Procedure101023820 yago:PsychologicalFeature100023100 yago:YagoPermanentlyLocatedEntity yago:Rule105846932 yago:WikicatAlgorithms |
| rdfs:comment | En informatique, l'algorithme de Davis–Putnam–Logemann–Loveland (DPLL) est un algorithme de backtracking, complet, de résolution du problème SAT. Le problème SAT est un problème important à la fois d'un point de vue théorique, en particulier en théorie de la complexité où il est le premier problème prouvé NP-complet et pratique puisqu'il peut apparaître lors de la résolution de problèmes de planification classique, model checking, ou encore diagnostic et jusqu'au configurateur d'un PC ou de son système d'exploitation[réf. nécessaire]. (fr) Het DPLL-algoritme (Davis-Putnam-Logemann-Loveland algoritme) is een algoritme voor het onderzoeken van de vervulbaarheid van een propositie in conjunctieve normaalvorm (dit probleem is ook bekend als CNF-SAT). Het algoritme werd gepubliceerd in 1962 door , Hilary Putnam, en als een verbetering van een eerder algoritme van Davis en Putnam uit 1960. Het algoritme maakt gebruik van backtracking indien nodig. Er bestaan allerlei verbeterde varianten van het DPLL-algoritme, zoals het , en . (nl) Davis-Putnam-Logemann-Lovelandアルゴリズム（DPLLアルゴリズム、英: Davis-Putnam-Logemann-Loveland algorithm）とは、数理論理学および計算機科学において、論理式の充足可能性を調べるアルゴリズムである。連言標準形で表現された命題論理式を対象とし、論理式を真（True）にできるかどうかを判定する。この判定問題はCNF-SATと呼ばれる。 このアルゴリズムは、1960年に発表されたデービス・パトナムのアルゴリズム（英: Davis–Putnam algorithm）の改良版として、1962年に（英語: Martin Davis）、（英語: George Logemann）、（英語: Donald W. Loveland）が発表した。 なお、文献によってはDPLLアルゴリズムのことをデービス・パトナムのアルゴリズムと呼ぶことがある。それぞれは異なった規則を使用し、正確には異なる。 (ja) DPLL (алгоритм Дэвиса — Патнема — Логемана — Лавленда) — полный алгоритм поиска с возвратом для решения задачи CNF-SAT — определения выполнимости булевых формул, записанных в конъюнктивной нормальной форме. Опубликован в 1962 году Мартином Дэвисом, Хилари Патнэмом, и как усовершенствование более раннего алгоритма Дэвиса — Патнема, основанного на правиле резолюций. Является высокоэффективным алгоритмом и спустя полвека сохраняет актуальность и используется в большинстве решателей для SAT и системах автоматического доказательства для фрагментов логики первого порядка. (ru) DPLL（Davis-Putnam-Logemann-Loveland）算法，是一種完備的、以回溯為基礎的算法，用於解決在合取範式（CNF）中命題邏輯的布爾可滿足性問題；也就是解決CNF-SAT问题。 它在1962年由馬丁·戴維斯、希拉里·普特南、和共同提出，作为早期的一种改进。戴維斯-普特南算法是戴維斯与普特南在1960年发展的一种算法。 DPLL是一种高效的程序，并且经过40多年还是最有效的SAT解法，以及很多一阶逻辑的自动定理证明的基础。 (zh) In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem. (en) El algoritmo DPLL/Davis-Putnam-Logemann-Loveland es un algoritmo completo basado en la vuelta atrás que sirve para decidir la satisfactibilidad de las fórmulas de lógica proposicional en una forma normal conjuntiva, es decir, para resolver el problema . El DPLL es un procedimiento muy eficiente y tras más de 40 años aún conforma la base de los solucionadores más eficaces de SAT, así como de muchos demostradores de teoremas para fragmentos de lógica de primer orden. (es) DPLL (Davis-Putnam-Logemann-Loveland) è un algoritmo di ricerca esaustiva, basato sul backtracking, utilizzato per decidere la soddisfacibilità booleana di formule di logica proposizionale in forma normale congiuntiva (CNF), problema noto come . Il DPLL è una procedura assai efficiente, e dopo più di 40 anni forma ancora la base dei più efficienti risolutori SAT completi, così come per molti dimostratori di teoremi per frammenti di logica del primo ordine. (it) O algoritmo DPLL/Davis-Putnam-Logemann-Loveland é um algoritmo completo baseado em backtracking (re-leitura ou voltar atrás) para decidir a satisfatibilidade das fórmulas de lógica proposicional na forma normal clausal, isto é, para solucionar o problema SAT. DPLL é um procedimento altamente eficiente, e forma a base para os mais eficientes solucionadores SAT e outros problemas NP-completos que podem ser reduzidos para o problema SAT, e também para muitos para os fragmentos da lógica de primeira ordem. (pt) Алгоритм Девіса-Патнема-Логемана-Лавленд — це повний алгоритм пошуку з поверненням для визначення здійсненності булевих формул, записаних в кон'юнктивній нормальній формі (КНФ) для вирішення завдання CNF-SAT. Алгоритм був опублікований в 1962 році Мартіном Девісом, Гіларі Патнемом, Джорджем Логеманом й Дональдом Лавленд та представляє собою удосконалення більш раннього алгоритму Девіса-Патнема, методу, заснованого на правилі резолюцій, розробленого Девісом та Патнемом в 1960 році. (uk) |
| rdfs:label | Algoritmo DPLL (es) DPLL algorithm (en) Algorithme DPLL (fr) DPLL (it) DPLLアルゴリズム (ja) DPLL-algoritme (nl) Algoritmo DPLL (pt) DPLL (ru) DPLL算法 (zh) DPLL алгоритм (uk) |
| owl:sameAs | freebase:DPLL algorithm yago-res:DPLL algorithm wikidata:DPLL algorithm dbpedia-es:DPLL algorithm dbpedia-fa:DPLL algorithm dbpedia-fr:DPLL algorithm dbpedia-it:DPLL algorithm dbpedia-ja:DPLL algorithm dbpedia-nl:DPLL algorithm dbpedia-pt:DPLL algorithm dbpedia-ru:DPLL algorithm dbpedia-sr:DPLL algorithm dbpedia-uk:DPLL algorithm dbpedia-zh:DPLL algorithm https://global.dbpedia.org/id/vkUb |
| prov:wasDerivedFrom | wikipedia-en:DPLL_algorithm?oldid=1094417709&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Dpll1.png wiki-commons:Special:FilePath/Dpll10.png wiki-commons:Special:FilePath/Dpll11.png wiki-commons:Special:FilePath/Dpll2.png wiki-commons:Special:FilePath/Dpll3.png wiki-commons:Special:FilePath/Dpll4.png wiki-commons:Special:FilePath/Dpll5.png wiki-commons:Special:FilePath/Dpll6.png wiki-commons:Special:FilePath/Dpll7.png wiki-commons:Special:FilePath/Dpll8.png wiki-commons:Special:FilePath/Dpll9.png |
| foaf:isPrimaryTopicOf | wikipedia-en:DPLL_algorithm |
| is dbo:knownFor of | dbr:George_Logemann dbr:Donald_W._Loveland dbr:Martin_Davis_(mathematician) |
| is dbo:wikiPageDisambiguates of | dbr:DPLL |
| is dbo:wikiPageRedirects of | dbr:Davis-Putnam-Logeman-Loveland_algorithm dbr:DPLL-Algorithm dbr:Davis-Logemann-Loveland_algorithm dbr:Davis-Putnam-Logemann-Loveland_algorithm dbr:Davis–Putnam–Logemann–Loveland_algorithm |
| is dbo:wikiPageWikiLink of | dbr:Proof_complexity dbr:Propositional_calculus dbr:Entscheidungsproblem dbr:List_of_algorithms dbr:Answer_set_programming dbr:List_of_important_publications_in_theoretical_computer_science dbr:Resolution_(logic) dbr:DPLL(T) dbr:Vampire_(theorem_prover) dbr:Propositional_proof_system dbr:Computer-assisted_proof dbr:George_Logemann dbr:Conflict-driven_clause_learning dbr:Davis-Putnam-Logeman-Loveland_algorithm dbr:Automated_theorem_proving dbr:DPLL dbr:List_of_New_York_University_faculty dbr:Hilary_Putnam dbr:Symbolic_artificial_intelligence dbr:Donald_W._Loveland dbr:Martin_Davis_(mathematician) dbr:Boolean_satisfiability_algorithm_heuristics dbr:Boolean_satisfiability_problem dbr:DPLL-Algorithm dbr:Chaff_algorithm dbr:SAT_solver dbr:Satisfiability_modulo_theories dbr:Satplan dbr:Loveland_(surname) dbr:Unit_propagation dbr:True_quantified_Boolean_formula dbr:Davis-Logemann-Loveland_algorithm dbr:Davis-Putnam-Logemann-Loveland_algorithm dbr:Davis–Putnam–Logemann–Loveland_algorithm |
| is dbp:knownFor of | dbr:George_Logemann dbr:Donald_W._Loveland dbr:Martin_Davis_(mathematician) |
| is foaf:primaryTopic of | wikipedia-en:DPLL_algorithm |
