Planning as Satisfiability

• Bounded-length plan finding can be posed directly as a SAT encoding

  • Set up k-length sequence of disjunctive actions (a1 V a2 V ….V an)
  • Impose constraints, which when satisfied, will ensure that some sub-sequence of the disjunctive sequence is a solution to the planning problem
    • The constraints set up lines of proof
      • State-space proofs
      • Causal proofs

[Kautz, McAllester, Selman, 96]

Previous slide

Next slide

Back to first slide

View graphic version