| 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)
|
![[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)