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]