An approach to automated planning that constructs a Boolean satisfiability problem for a bounded planning horizon, solves it and decodes a satisfying assignment into a plan. A typical encoding has time-indexed action occurrences and planning fluents, initial and goal clauses, action precondition axioms, state-transition constraints and action exclusion axioms. Sequential and parallel encodings have different notions of a step.
Henry Kautz and Bart Selman introduced planning as satisfiability in their 1992 paper.[ref]
Planning as satisfiability by Henry Kautz and Bart Selman. ECAI 1992, pp. 359–363; publication listed in the author's Cornell bibliography
New to topics? Read the docs here!