
18.3 Planning Graphs 443
Strong-Conformant-Davis-Putnam()
return Generate-Weak(,∅)
end
Generate-Weak(φ,µ)
if φ =∅then return Test-if-Strong(µ)
if ∅∈φ then return False
if a unit clause L occurs in φ then
return Generate-Weak(assign(L,φ),µ ∪{L})
P ← an atom occurring in φ
return Generate-Weak(assign(P,φ),µ ∪{P})or
Generate-Weak(assign(¬P,φ),µ ∪{¬P})
end
Test-if-Strong(µ)
for each assignment µ
such that µ ⊆ µ
do
if
is not satisfiable then exit with µ
return False
end
Figure 18.1 Algorithm for generating and testing strong conformant solutions.
reformulated as a QBF rather than in propositional logic. QBF solvers are employed
in place of SAT solvers. QBF logic ...