aima.logic.propositional.algorithms
Class DPLL

java.lang.Object
  aima.logic.propositional.algorithms.DPLL

public class DPLL
extends java.lang.Object

Author:

Ravi Mohan

Nested Class Summary

class

DPLL.SymbolValuePair

Constructor Summary

DPLL()

Method Summary

java.util.List<Sentence>	clausesWithNonTrueValues(java.util.List<Sentence> clauseList, Model model)
boolean	dpllSatisfiable(Sentence s)
boolean	dpllSatisfiable(Sentence s, Model m)
boolean	dpllSatisfiable(java.lang.String string)
DPLL.SymbolValuePair	findPureSymbolValuePair(java.util.List<Sentence> clauseList, Model model, java.util.List symbols)
java.util.Set	findUnitClauses(java.util.Set clauses, Symbol symbol, Model m)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

DPLL

public DPLL()

Method Detail

dpllSatisfiable

public boolean dpllSatisfiable(Sentence s)

dpllSatisfiable

public boolean dpllSatisfiable(java.lang.String string)

dpllSatisfiable

public boolean dpllSatisfiable(Sentence s,
                               Model m)

findUnitClauses

public java.util.Set findUnitClauses(java.util.Set clauses,
                                     Symbol symbol,
                                     Model m)

clausesWithNonTrueValues

public java.util.List<Sentence> clausesWithNonTrueValues(java.util.List<Sentence> clauseList,
                                                         Model model)

findPureSymbolValuePair

public DPLL.SymbolValuePair findPureSymbolValuePair(java.util.List<Sentence> clauseList,
                                                    Model model,
                                                    java.util.List symbols)