---
title: "Automatic SAT-Compilation of Planning Problems"
authors:
  - "Michael D. Ernst"
  - "Todd D. Millstein"
  - "Daniel S. Weld"
doi: ""
url: "https://ijcai.org/proceedings/1997/169"
pdf: "https://ijcai.org/proceedings/1997/0169.pdf"
venue: "Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence"
year: 1997
pages: "1169-1176"
track: "Planning and Scheduling"
keywords:
---

# Automatic SAT-Compilation of Planning Problems

Michael D. Ernst, Todd D. Millstein, Daniel S. Weld

*Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence*, pages 1169-1176.

## Abstract

Recent work by Kautz et al. provides tantalizing evidence that large, classical planning problems may be efficiently solved by translating them into propositional satisfiability problems, using stochastic search techniques , and translating the resulting truth assignments back into plans for the original problems. We explore the space of such transformations , providing a simple framework that generates eight major encodings (generated by selecting one of four action representations and one of two frame axioms) and a number of subsidiary ones. We describe a fully-implemented compiler that can generate each of these encodings, and we test the compiler on a suite of STRIPS planning problems in order to determine which encodings have the best properties.