aima.core.logic.propositional.inference

Interface DPLL

All Known Implementing Classes:

DPLLSatisfiable, OptimizedDPLL

public interface DPLL

Interface describing main API of the DPLL algorithm as described in Figure 7.17 but not how it should be implemented. This is to allow for experimentation with different implementations to explore different performance optimization strategies as described on p.g.s 261-262 of AIMA3e (i.e. 1. component analysis, 2. variable and value ordering, 3. intelligent backtracking, 4. random restarts, and 5. clever indexing).

Author:

Ciaran O'Reilly

Method Summary

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.
boolean	isEntailed(KnowledgeBase kb, Sentence alpha) Determine if KB |= α, i.e.

Method Detail

dpllSatisfiable

boolean dpllSatisfiable(Sentence s)

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

Parameters:

s - a sentence in propositional logic.

Returns:

true if the sentence is satisfiable, false otherwise.

dpll

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

DPLL(clauses, symbols, model)

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

boolean isEntailed(KnowledgeBase kb,
                   Sentence alpha)

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

Parameters:

kb - a Knowledge Base in propositional logic.

alpha - a propositional sentence.

Returns:

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