“ SAT in polynomial time – Yes, it’s possible!! ” You are given Hint. (a or b) a
ID: 3771136 • Letter: #
Question
“SAT in polynomial time – Yes, it’s possible!!” You are given
Hint. (a or b) and (not b or not c) is equivalent to writing: (a or not c).
following format: (x1 or x2) and (x3 or x4) ..... That is, the SAT formula has a list of conjunctions (AND
a SAT formula of the
symbol), and each conjunction consists of exactly two disjunctions (literal connected by OR connector).
Describe an efficient algorithm to find an assignment of truth-values to literals such that the formula is
true, or report that the formula is not satisfiable. Surely, your “efficient” algorithm should run in
polynomial time
Hint. (a or b) and (not b or not c) is equivalent to writing: (a or not c).
subject
design analysis algorithm
Explanation / Answer
/*
literal -> single Atoms are literal
Example : P
not(P)
Poynomial Time Algorithm Derived by Davis –Putnam –Loveland –Logemann
*/
dpll(F, literal){
remove clauses containing literal
if (F contains no clauses)
return true;
shorten clauses containing not(literal)
if (F contains empty clause)
return false;
if (F contains a unit or pure L):
return dpll(F,L)
choose V in F;
if (dpll(F, not(V)))
return true;
return dpll(F, V);
}
Related Questions
Navigate
Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.