| dbo:abstract
|
- In computer science, conflict-driven clause learning (CDCL) is an algorithm for solving the Boolean satisfiability problem (SAT). Given a Boolean formula, the SAT problem asks for an assignment of variables so that the entire formula evaluates to true. The internal workings of CDCL SAT solvers were inspired by DPLL solvers. The main difference between CDCL and DPLL is that CDCL's back jumping is non-chronological. Conflict-driven clause learning was proposed by Marques-Silva and Sakallah (1996, 1999) and Bayardo and Schrag (1997). (en)
- Алгоритм CDCL (англ. conflict-driven clause learning — «управляемое конфликтами обучение дизъюнктам») — основанный на алгоритме DPLL эффективный решатель (NP-полных) задач выполнимости булевых формул (SAT-решатель). Основная структура данных в CDCL-решателях — импликационный граф, фиксирующий назначения переменным, а другой особенностью является использование нехронологического возврата и запоминание дизъюнктов в ходе анализа конфликта. Алгоритм был предложен (англ. João Marques-Silva) и (англ. Karem A. Sakallah) в 1996 году и независимо (англ. Roberto J. Bayardo) и (англ. Robert C. Schrag) в 1997 году. (ru)
|
| dbo:thumbnail
| |
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 9976 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| rdfs:comment
|
- In computer science, conflict-driven clause learning (CDCL) is an algorithm for solving the Boolean satisfiability problem (SAT). Given a Boolean formula, the SAT problem asks for an assignment of variables so that the entire formula evaluates to true. The internal workings of CDCL SAT solvers were inspired by DPLL solvers. The main difference between CDCL and DPLL is that CDCL's back jumping is non-chronological. Conflict-driven clause learning was proposed by Marques-Silva and Sakallah (1996, 1999) and Bayardo and Schrag (1997). (en)
- Алгоритм CDCL (англ. conflict-driven clause learning — «управляемое конфликтами обучение дизъюнктам») — основанный на алгоритме DPLL эффективный решатель (NP-полных) задач выполнимости булевых формул (SAT-решатель). Основная структура данных в CDCL-решателях — импликационный граф, фиксирующий назначения переменным, а другой особенностью является использование нехронологического возврата и запоминание дизъюнктов в ходе анализа конфликта. (ru)
|
| rdfs:label
|
- Conflict-driven clause learning (en)
- Алгоритм CDCL (ru)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:depiction
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
