Direct generation of SAT encodings

• Bounded-length plan finding can be posed directly as a SAT encoding (skipping the refinement step).

  • Set up k-length sequence of disjunctive actions (a1 V a2 V ….V an)
    • In effect, a direct naïve refinement is used (monotonic, complete, but not progressive)
  • 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