aima.core.logic.propositional.inference

Class SATPlan

java.lang.Object

aima.core.logic.propositional.inference.SATPlan

public class SATPlan
extends java.lang.Object

Artificial Intelligence A Modern Approach (3rd Edition): page 261.

 
 function SATPlan(init, transition, goal, Tmax) returns solution or failure
   inputs: init, transition, goal, constitute a description of the problem
           Tmax, an upper limit for plan length
   
   for t = 0 to Tmax do
       cnf ←  TRANSLATE-TO-SAT(init, transition, goal, t)
       model ← SAT-SOLVER(cnf)
       if model is not null then
           return EXTRACT-SOLUTION(model)
   return failure
 
 

Figure 7.22 The SATPlan algorithm. The planning problem is translated into a CNF sentence in which the goal is asserted to hold at a fixed time step t and axioms are included for each time step up to t. If the satisfiability algorithm finds a model, then a plan is extracted by looking at those proposition symbols that refer to actions and are assigned true in the model. If no model exists, then the process is repeated with the goal moved one step later.

Author:

Ciaran O'Reilly

Constructor Summary

Constructors

Constructor and Description
SATPlan(SATSolver satSolver, aima.core.logic.propositional.inference.SATPlan.SolutionExtractor solutionExtractor)

Method Summary

Modifier and Type	Method and Description
java.util.List<Action>	satPlan(aima.core.logic.propositional.inference.SATPlan.Describe init, aima.core.logic.propositional.inference.SATPlan.Describe transition, aima.core.logic.propositional.inference.SATPlan.Describe goal, int tMax) function SATPlan(init, transition, goal, Tmax) returns solution or failure
protected java.util.Set<Clause>	translateToSAT(aima.core.logic.propositional.inference.SATPlan.Describe init, aima.core.logic.propositional.inference.SATPlan.Describe transition, aima.core.logic.propositional.inference.SATPlan.Describe goal, int t)

Methods inherited from class java.lang.Object

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

Constructor Detail

SATPlan

public SATPlan(SATSolver satSolver,
               aima.core.logic.propositional.inference.SATPlan.SolutionExtractor solutionExtractor)

Method Detail

satPlan

public java.util.List<Action> satPlan(aima.core.logic.propositional.inference.SATPlan.Describe init,
                                      aima.core.logic.propositional.inference.SATPlan.Describe transition,
                                      aima.core.logic.propositional.inference.SATPlan.Describe goal,
                                      int tMax)

function SATPlan(init, transition, goal, T_max) returns solution or failure

Parameters:

init - provides a collection of assertions about the initial state.

transition - provides the successor-state axioms for all possible actions at each time step up to some maximum t.

goal - provides the assertion that the goal is achieved at time t.

tMax - the maximum number of time steps in which the goal is to be achieved in.

Returns:

a list of actions describing a solution for the given problem or null if no solution is found (i.e failure)

translateToSAT

protected java.util.Set<Clause> translateToSAT(aima.core.logic.propositional.inference.SATPlan.Describe init,
                                               aima.core.logic.propositional.inference.SATPlan.Describe transition,
                                               aima.core.logic.propositional.inference.SATPlan.Describe goal,
                                               int t)