SATPlan (source code)
= SATPlan
{c}
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.<Planning as satisfiability by Henry Kautz and Bart Selman>[ECAI 1992, pp. 359–363; publication listed in the author's Cornell bibliography]{ref}
Back to article page
