In the SATPLAN algorithm in Figure, each call to the satisfiability algorithm asserts a goal g ^T where T ranges from 0 to T_max. Suppose instead that the satisfiability algorithm is called only once, with the goal g⁰ V g¹ V…. Vg ^T _max

a. Will this always return a plan if one exists with length less than or equal to Tm?

b. Does this approach introduce any new spurious “solutions”?

c. Discuss how one might modify a satisfiability algorithm such as WALKSAT so that it finds short solutions (if they exist) when given a disjunctive goal of this form.

Transcribed Image Text:

function SATPLAN(problem, T max) returns solution or failure inputs: problem, a planning problem Tmax, an upper limit for plan length for T = 0 to T max do enf, mapping - TRANSLATE-TO-SAT(problem, T) assignment - SAT-SOLVER(Cnf) if assignment is not null then return EXTRACT-SOLUTION(assignment, mapping) return failure