The DPLL satisfiability algorithm is a backtracking search algorithm with 3 heuristic improvements: PURE-SYMBOLS, UNIT-CLAUSES, and EARLY
Question:
The DPLL satisfiability algorithm is a backtracking search algorithm with 3 heuristic improvements: PURE-SYMBOLS, UNIT-CLAUSES, and EARLY TERMINATION. This question connects these improvements to more general CSP techniques used with backtracking search.
a. In the following CNF expression, which symbols are pure and what value does the PURE-SYMBOLS heuristic assign to those symbols?
(C ∨ D) ∧ (C ∨ ¬A) ∧ (¬D ∨ A) ∧ (¬B ∨ A)
b. Which of the following CSP techniques are equivalent to the PURE-SYMBOLS and UNIT-CLAUSES heuristics when applied to SAT for CNF sentences?
MINIMUM-REMAINING-VALUES
FORWARD-CHECKING
LEAST-CONSTRAINING-VALUE
BACKTRACKING
No equivalent CSP technique
c. DPLL performs early termination in two steps: SUCCESS-DETECTION and FAILUREDETECTION. First, SUCCESS-DETECTION checks to see if all clauses evaluate to true. If so, the sentence is satisfiable and any unassigned propositional symbols can be assigned arbitrarily. Next, FAILURE-DETECTION checks if any clause evaluates to false. In this case the sentence is unsatisfiable and this branch of the search can be pruned. Which, if any, of these forms of early termination does the general CSP backtracking algorithm use?
Step by Step Answer:
Artificial Intelligence A Modern Approach
ISBN: 9780134610993
4th Edition
Authors: Stuart Russell, Peter Norvig