1
$\begingroup$

We know DPLL algorithm is backtracking + unit propagation + pure literal rule.

I have an example. There is one example to solve following Satisfiability problem with DPLL. if assign of "0" to variables is prior to assign "1" to variables, Which of Unit Clause (UC) or Pure Literal (PL) is used to solve this specific example?

$\{\lnot A \lor B \lor C\}, \{A \lor \lnot B \lor C\}, \{A \lor B \lor \lnot C\}, \{A \lor B \lor C\}$

Olympiad Solution is: PL and UC.

Our Solution is just UC.

Who can satisfy me why Olympiad solution is correct ?!

Unit propagation is not possible as there are no unit clauses.

Pure literal rule is not applicable as there is no literals that occur only positively or only negatively.

Update: I think in node (3) we can user PL or UC. Isn't it? enter image description here

|cite|improve this question
$\endgroup$
  • $\begingroup$ Note that this question does not seem to have anything to do with AI; it's a pure logics question. $\endgroup$ – Raphael♦ Jun 21 '16 at 9:03
  • $\begingroup$ As far as I can see, you are correct. Assigning variables as you described, false first then backtracking to true if a conflict occurs, you arrive at a solution using only unit propagation. Pure literal elimination is never invoked. This is the case regardless of the variable assignment order as the clause-variable graph is just one big automorphism. $\endgroup$ – Kyle Jones Jun 21 '16 at 15:58
  • $\begingroup$ @KyleJones Thanks, but I think there is a trick in this question. $\endgroup$ – Sara PhD Jun 21 '16 at 18:10
  • $\begingroup$ @KyleJones please see my update. $\endgroup$ – Sara PhD Jun 24 '16 at 0:14
  • $\begingroup$ The pure literal rule is applicable to (3), but it never would be applied because the unit rule is always applied first in DPLL. $\endgroup$ – Kyle Jones Jun 24 '16 at 7:30
3
$\begingroup$

If you use the original specification of the DPLL algorithm, in which the unit rule is applied to a fixed point and then the pure literal rule, then only the unit rule is needed to reach a satisfying assignment. If the rule order is reversed then the pure literal rule is used to eliminate the final unsatisfied clause.

DPLL is a complete and sound algorithm for deciding Boolean satisfiability even if the pure literal rule is removed. In practice, pure literals are typically removed only during the preprocessing of a SAT instance, where the formula is simplied as much as possible before beginning recursive search. This is because detecting pure literals during search is computationally expensive enough to more than offset any expected runtime gains.

|cite|improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.