Browse using
OpenLink Faceted Browser
OpenLink Structured Data Editor
LodLive Browser
Formats
RDF:
N-Triples
N3
Turtle
JSON
XML
OData:
Atom
JSON
Microdata:
JSON
HTML
Embedded:
JSON
Turtle
Other:
CSV
JSON-LD
Faceted Browser
Sparql Endpoint
About:
DPLL algorithm
An Entity of Type:
Thing
,
from Named Graph:
http://dbpedia.org
,
within Data Space:
dbpedia.org
Algorithm for solving the CNF-SAT problem
Property
Value
dbo:
description
algorisme per resoldre el problema CNF-SAT
(ca)
algorithm for solving the CNF-SAT problem
(en)
algoritmo per la risoluzione di CNF-SAT
(it)
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:
wikiPageWikiLink
dbr
:Backtracking
dbr
:Model_checking
dbr
:Implication_graph
dbr
:Unit_propagation
dbr
:Stålmarck's_method
dbr
:Communications_of_the_ACM
dbr
:Diagnosis_(artificial_intelligence)
dbr
:Resolution_(logic)
dbr
:Satisfiability_modulo_theories
dbr
:First-order_logic
dbr
:Automated_theorem_proving
dbr
:Propositional_logic
dbr
:Donald_W._Loveland
dbc
:Articles_with_example_pseudocode
dbr
:Logic
dbr
:Binary_decision_diagram
dbr
:Completeness_(logic)
dbr
:Proof_complexity
dbr
:SAT_solver
dbr
:Martin_Davis_(mathematician)
dbr
:Computer_science
dbr
:Mathematical_theory
dbc
:Automated_theorem_proving
dbr
:Truth_value
dbr
:Computational_complexity_theory
dbr
:Automated_planning_and_scheduling
dbr
:Boolean_satisfiability_problem
dbr
:Hilary_Putnam
dbr
:Search_algorithm
dbr
:Conjunctive_normal_form
dbr
:Heuristic_function
dbr
:Journal_of_the_ACM
dbr
:Binary_tree
dbc
:Constraint_programming
dbc
:SAT_solvers
dbr
:Davis–Putnam_algorithm
dbr
:Propositional_variable
dbr
:GRASP_(SAT_solver)
dbr
:DPLL(T)
dbr
:Backjumping
dbr
:Herbrandization
dbr
:George_Logemann
dbr
:NP-complete
dbr
:Conflict-Driven_Clause_Learning
dbr
:Short-circuiting_operator
dbr
:Polarity_(mathematical_logic)
dbr
:ZChaff
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
:Reflist
dbt
:Cite_journal
dbt
:Infobox_algorithm
dbt
:Algorithm-end
dbt
:Citation_needed
dbt
:Algorithm-begin
dbt
:Short_description
dct:
subject
dbc
:Articles_with_example_pseudocode
dbc
:Automated_theorem_proving
dbc
:Constraint_programming
dbc
:SAT_solvers
rdfs:
label
DPLL algorithm
(en)
Algoritmo DPLL
(es)
Algorithme DPLL
(fr)
DPLLアルゴリズム
(ja)
DPLL
(it)
DPLL-algoritme
(nl)
Algoritmo DPLL
(pt)
DPLL
(ru)
DPLL алгоритм
(uk)
DPLL算法
(zh)
owl:
sameAs
yago-res
:DPLL algorithm
freebase
:DPLL algorithm
wikidata
:DPLL algorithm
dbpedia-it
:DPLL algorithm
dbpedia-nl
:DPLL algorithm
dbpedia-fr
:DPLL algorithm
dbpedia-zh
:DPLL algorithm
dbpedia-ja
:DPLL algorithm
dbpedia-pt
:DPLL algorithm
dbpedia-es
:DPLL algorithm
dbpedia-fa
:DPLL algorithm
dbpedia-ru
:DPLL algorithm
dbpedia-sr
:DPLL algorithm
dbpedia-uk
:DPLL algorithm
dbpedia-global
:DPLL algorithm
prov:
wasDerivedFrom
wikipedia-en
:DPLL_algorithm?oldid=1292217523&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
:Donald_W._Loveland
dbr
:Martin_Davis_(mathematician)
dbr
:George_Logemann
is
dbo:
wikiPageDisambiguates
of
dbr
:DPLL
is
dbo:
wikiPageRedirects
of
dbr
:Davis-Logemann-Loveland_algorithm
dbr
:Davis-Putnam-Logeman-Loveland_algorithm
dbr
:Davis-Putnam-Logemann-Loveland_algorithm
dbr
:Davis–Putnam–Logemann–Loveland_algorithm
dbr
:DPLL-Algorithm
is
dbo:
wikiPageWikiLink
of
dbr
:Unit_propagation
dbr
:True_quantified_Boolean_formula
dbr
:Resolution_(logic)
dbr
:Satisfiability_modulo_theories
dbr
:Automated_theorem_proving
dbr
:Propositional_calculus
dbr
:Donald_W._Loveland
dbr
:Computer-assisted_proof
dbr
:Answer_set_programming
dbr
:Symbolic_artificial_intelligence
dbr
:Proof_complexity
dbr
:Propositional_proof_system
dbr
:SAT_solver
dbr
:Martin_Davis_(mathematician)
dbr
:Boolean_satisfiability_problem
dbr
:Entscheidungsproblem
dbr
:Hilary_Putnam
dbr
:DPLL
dbr
:Satplan
dbr
:List_of_algorithms
dbr
:Chaff_algorithm
dbr
:List_of_New_York_University_faculty
dbr
:Vampire_(theorem_prover)
dbr
:DPLL(T)
dbr
:Boolean_satisfiability_algorithm_heuristics
dbr
:George_Logemann
dbr
:Conflict-driven_clause_learning
dbr
:Loveland_(surname)
dbr
:List_of_important_publications_in_theoretical_computer_science
dbr
:Davis-Logemann-Loveland_algorithm
dbr
:Davis-Putnam-Logeman-Loveland_algorithm
dbr
:Davis-Putnam-Logemann-Loveland_algorithm
dbr
:Davis–Putnam–Logemann–Loveland_algorithm
dbr
:DPLL-Algorithm
is
dbp:
knownFor
of
dbr
:Donald_W._Loveland
dbr
:George_Logemann
is
foaf:
primaryTopic
of
wikipedia-en
:DPLL_algorithm
This content was extracted from
Wikipedia
and is licensed under the
Creative Commons Attribution-ShareAlike 4.0 International