thanks in advance! SAT is the language of Boolean expressions in conjunctive nor
ID: 651723 • Letter: T
Question
thanks in advance!
SAT is the language of Boolean expressions in conjunctive normal form (CNF) that are satisfiable. CNF means that we haw conjunctions of disjunctions of literals, in other words, we have ANDs of ORs of variables and negated variables. The Boolean expression is satisfiable if one can assign truth values true (1) or false (0) to the variable to make the whole expression true. An interesting question is how deciding the existence of a solution and actually finding a solution are related. For SAT. it turns out that finding a satisfying assignment is not much more difficult than deciding whether there exist a satisfying assignment. This is so. because SAT is self-reducible. We have seen reductions from one problem to another one. Here we want to reduce SAT to itself, but herby asking easier and easier questions. Consider this as a hint on how to solve the following task Design an algorithm A to find a satisfying assignment for a Boolean expression phi in CNF with the help of a decider. Your input is a Boolean expression phi in CNF. Assume, you know that d Ls satisfiable. Your algorithm should be efficient, i.e. running in polynomial time with the help of a magician. Your algorithm is allowed to ask the magician an arbitrary number of questions. Each question consists of a Boolean expression phi in CNF. The magician answers in no tune whether phi is satisfiable. Your algo-rithm finds a satisfying assignment. The intuitive argument Ls now this. Assume satisfiability could be decided easily. Then you could always decide it without asking the magician. Then you had an algorithm to find a satisfying assignment efficiently. To describe your algorithm A. tell how to find the questions to ask.Explanation / Answer
dpll_2(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;
choose V in F;
if (dpll_2(F, not (V)))return true;
return dpll_2(F, V);
}
Related Questions
Navigate
Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.