 Planning as satisfiability by Henry Kautz and Bart Selman

Author-hosted paper: www.cs.cornell.edu/selman/papers/pdf/92.ecai.satplan.pdf

Author bibliography: www.cs.cornell.edu/selman/papers/

Published in Proceedings of ECAI 1992, pp. 359–363. The paper introduced the SATPlan approach. The bounded model, state-transition formulas and deletion-sensitive proof used here are given explicitly rather than relying on a copied encoding.