aima.core.logic.propositional.inference

Class OptimizedDPLL

java.lang.Object

aima.core.logic.propositional.inference.OptimizedDPLL

All Implemented Interfaces:

DPLL

public class OptimizedDPLL
extends java.lang.Object
implements DPLL

Constructor Summary

Constructors

Constructor and Description
OptimizedDPLL()

Method Summary

Modifier and Type	Method and Description
protected boolean	callDPLL(java.util.Set<Clause> clauses, java.util.List<PropositionSymbol> symbols, Model model, PropositionSymbol p, boolean value)
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 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)

Methods inherited from class java.lang.Object

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

Constructor Detail

OptimizedDPLL

public OptimizedDPLL()

Method Detail

dpllSatisfiable

public boolean dpllSatisfiable(Sentence s)

Description copied from interface: DPLL

DPLL-SATISFIABLE?(s)
Checks the satisfiability of a sentence in propositional logic.

Specified by:

dpllSatisfiable in interface DPLL

Parameters:

s - a sentence in propositional logic.

Returns:

true if the sentence is satisfiable, false otherwise.

dpll

public boolean dpll(java.util.Set<Clause> clauses,
                    java.util.List<PropositionSymbol> symbols,
                    Model model)

DPLL(clauses, symbols, model)

Specified by:

dpll in interface DPLL

Parameters:

clauses - the set of clauses.

symbols - a list of unassigned symbols.

model - contains the values for assigned symbols.

Returns:

true if the model is satisfiable under current assignments, false otherwise.

isEntailed

public boolean isEntailed(KnowledgeBase kb,
                          Sentence alpha)

Determine if KB |= α, i.e. alpha is entailed by KB.

Specified by:

isEntailed in interface DPLL

Parameters:

kb - a Knowledge Base in propositional logic.

alpha - a propositional sentence.

Returns:

true, if α is entailed by KB, false otherwise.

getPropositionSymbolsInSentence

protected java.util.List<PropositionSymbol> getPropositionSymbolsInSentence(Sentence s)

callDPLL

protected boolean callDPLL(java.util.Set<Clause> clauses,
                           java.util.List<PropositionSymbol> symbols,
                           Model model,
                           PropositionSymbol p,
                           boolean value)

findPureSymbol

protected Pair<PropositionSymbol,java.lang.Boolean> findPureSymbol(java.util.List<PropositionSymbol> symbols,
                                                                   java.util.Set<Clause> clauses,
                                                                   Model model)

AIMA3e p.g. 260:
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.

Parameters:

symbols - a list of currently unassigned symbols in the model (to be checked if pure or not).

clauses -

model -

Returns:

a proposition symbol and value pair identifying a pure symbol and a value to be assigned to it, otherwise null if no pure symbol can be identified.

findUnitClause

protected Pair<PropositionSymbol,java.lang.Boolean> findUnitClause(java.util.Set<Clause> clauses,
                                                                   Model model)

AIMA3e p.g. 260:
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.

Parameters:

clauses -

model -

Returns:

a proposition symbol and value pair identifying a unit clause and a value to be assigned to it, otherwise null if no unit clause can be identified.

minus

protected java.util.List<PropositionSymbol> minus(java.util.List<PropositionSymbol> symbols,
                                                  PropositionSymbol p)