public class DPLLSatisfiable extends java.lang.Object implements DPLL
function DPLL-SATISFIABLE?(s) returns true or false
inputs: s, a sentence in propositional logic.
clauses ← the set of clauses in the CNF representation of s
symbols ← a list of the proposition symbols in s
return DPLL(clauses, symbols, {})
--------------------------------------------------------------------------------
function DPLL(clauses, symbols, model) returns true or false
if every clause in clauses is true in model then return true
if some clause in clauses is false in model then return false
P, value ← FIND-PURE-SYMBOL(symbols, clauses, model)
if P is non-null then return DPLL(clauses, symbols - P, model ∪ {P = value})
P, value ← FIND-UNIT-CLAUSE(clauses, model)
if P is non-null then return DPLL(clauses, symbols - P, model ∪ {P = value})
P ← FIRST(symbols); rest ← REST(symbols)
return DPLL(clauses, rest, model ∪ {P = true}) or
DPLL(clauses, rest, model ∪ {P = false})
Figure 7.17 The DPLL algorithm for checking satisfiability of a sentence in
propositional logic. The ideas behind FIND-PURE-SYMBOL and FIND-UNIT-CLAUSE
are described in the test; each returns a symbol (or null) and the truth
value to assign to that symbol. Like TT-ENTAILS?, DPLL operates over partial
models.| Constructor and Description |
|---|
DPLLSatisfiable() |
| Modifier and Type | Method and Description |
|---|---|
boolean |
dpll(java.util.Set<Clause> clauses,
java.util.List<PropositionSymbol> symbols,
Model model)
DPLL(clauses, symbols, model)
|
boolean |
dpllSatisfiable(Sentence s)
DPLL-SATISFIABLE?(s)
Checks the satisfiability of a sentence in propositional logic. |
protected boolean |
everyClauseTrue(java.util.Set<Clause> clauses,
Model model) |
protected Pair<PropositionSymbol,java.lang.Boolean> |
findPureSymbol(java.util.List<PropositionSymbol> symbols,
java.util.Set<Clause> clauses,
Model model)
AIMA3e p.g.
|
protected Pair<PropositionSymbol,java.lang.Boolean> |
findUnitClause(java.util.Set<Clause> clauses,
Model model)
AIMA3e p.g.
|
protected java.util.List<PropositionSymbol> |
getPropositionSymbolsInSentence(Sentence s) |
boolean |
isEntailed(KnowledgeBase kb,
Sentence alpha)
Determine if KB |= α, i.e.
|
protected java.util.List<PropositionSymbol> |
minus(java.util.List<PropositionSymbol> symbols,
PropositionSymbol p) |
protected boolean |
someClauseFalse(java.util.Set<Clause> clauses,
Model model) |
public boolean dpllSatisfiable(Sentence s)
dpllSatisfiable in interface DPLLs - a sentence in propositional logic.public boolean dpll(java.util.Set<Clause> clauses, java.util.List<PropositionSymbol> symbols, Model model)
public boolean isEntailed(KnowledgeBase kb, Sentence alpha)
isEntailed in interface DPLLkb - a Knowledge Base in propositional logic.alpha - a propositional sentence.protected java.util.List<PropositionSymbol> getPropositionSymbolsInSentence(Sentence s)
protected Pair<PropositionSymbol,java.lang.Boolean> findPureSymbol(java.util.List<PropositionSymbol> symbols, java.util.Set<Clause> clauses, Model model)
Pure symbol heuristic: A pure symbol is a symbol that always appears with the same "sign" in all clauses. For example, in the three clauses (A | ~B), (~B | ~C), and (C | A), the symbol A is pure because only the positive literal appears, B is pure because only the negative literal appears, and C is impure. It is easy to see that if a sentence has a model, then it has a model with the pure symbols assigned so as to make their literals true, because doing so can never make a clause false. Note that, in determining the purity of a symbol, the algorithm can ignore clauses that are already known to be true in the model constructed so far. For example, if the model contains B=false, then the clause (~B | ~C) is already true, and in the remaining clauses C appears only as a positive literal; therefore C becomes pure.
symbols - a list of currently unassigned symbols in the model (to be
checked if pure or not).clauses - model - protected Pair<PropositionSymbol,java.lang.Boolean> findUnitClause(java.util.Set<Clause> clauses, Model model)
Unit clause heuristic: A unit clause was defined earlier as a clause with just one literal. In the context of DPLL, it also means clauses in which all literals but one are already assigned false by the model. For example, if the model contains B = true, then (~B | ~C) simplifies to ~C, which is a unit clause. Obviously, for this clause to be true, C must be set to false. The unit clause heuristic assigns all such symbols before branching on the remainder. One important consequence of the heuristic is that any attempt to prove (by refutation) a literal that is already in the knowledge base will succeed immediately. Notice also that assigning one unit clause can create another unit clause - for example, when C is set to false, (C | A) becomes a unit clause, causing true to be assigned to A. This "cascade" of forced assignments is called unit propagation. It resembles the process of forward chaining with definite clauses, and indeed, if the CNF expression contains only definite clauses then DPLL essentially replicates forward chaining.
clauses - model - protected java.util.List<PropositionSymbol> minus(java.util.List<PropositionSymbol> symbols, PropositionSymbol p)