Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:dpll_algorithm_for_sat [2008/03/13 17:45] vkuncak |
sav08:dpll_algorithm_for_sat [2008/03/13 17:46] vkuncak |
||
---|---|---|---|
Line 28: | Line 28: | ||
Note: for each unit clause and other clause we can perform unit resolution at most once (variable disappears) | Note: for each unit clause and other clause we can perform unit resolution at most once (variable disappears) | ||
* BCP is polynomial procedure | * BCP is polynomial procedure | ||
+ | |||
+ | We do not need to keep literals that are subset of existing ones: | ||
+ | <code> | ||
+ | def RemoveSubsumed(S : Set[Clause]) : Set[Clause] = | ||
+ | if there are C1,C2 in S such that C1 subset C2 | ||
+ | then RemoveSubsumes(S - {C2}) | ||
+ | else S | ||
+ | </code> | ||
+ | In particular, when we apply unit resolution, the original clause can be deleted. | ||
===== DPLL Recursively ===== | ===== DPLL Recursively ===== | ||
Line 39: | Line 48: | ||
val P = pick variable from FV(S') | val P = pick variable from FV(S') | ||
DPLL(F' union {p}) or DPLL(F' union {Not(p)}) | DPLL(F' union {p}) or DPLL(F' union {Not(p)}) | ||
- | </code> | ||
- | |||
- | <code> | ||
- | def RemoveSubsumed(S : Set[Clause]) : Set[Clause] = | ||
- | if there are C1,C2 in S such that C1 subset C2 | ||
- | then RemoveSubsumes(S - {C2}) | ||
- | else S | ||
</code> | </code> | ||