Review-Automatic SAT-Compilation of Planning Problems

Automatic SAT-Compilation of Planning Problems
Ernst, Millstein, and Weld

*Summary
The authors present MEDIC, a system which utilizes one of eight different techniques to translate traditional STRIPS style planning problems into SAT problems.  Furthermore, the authors compare each of these eight methods of translation against one another and against the performance of hand coded translations done by others.

*Two Most Important Ideas
One of the most important ideas of this paper is that it is possible to construct compilers that translate STRIPS style problems into equivalent SAT problems and that the resulting SAT encodings empirically demonstrate performance "within a factor of two" of hand coded translations.  This is important because it demonstrates that researchers can continue to think about planning problems in an intuitive and comfortable way and, with out a huge investment of labor, test to see if their planning problem is perhaps tractable as a SAT problem.

The second important idea of the paper is that the asymptotic worst case analysis of the number of variables for various encoding and translation schemes is not an accurate predictor of performance.  As the authors point out they would have expected "bitwise encodings to have the smallest number of variables and the regular encodings to have the largest" however they found that this was not the case.  Rather they found that regular explanatory encoding had some of the fewest variables.  This is particularly important because such an encoding was at first dismissed " as impractical" by [Kautz and Selman].  This is an important idea first in that it demonstrates the need for experimentation despite asymptotic analysis of worst case, and second in that it again demonstrates the practice speedup that can be archived through various tricks which reduce the expected if not the worst case run time (such as typing in this case).

*Flaws
I would have appreciated a clear example of a simple STRIPS planning problem and the resulting SAT problem, not just snippets for various encoding schemes.  Perhaps such an example existed in the [Kautz and Selman, 1996] paper, but without it I had a hard time visualizing the problem at hand.

*Open Questions
It seems to me that since one of the best methods for translating the STRIPS problems into SAT problems was also one of the worst in terms of number of variables in the worst case, that it would be nice if there was a quick and cheap analysis of the problem that could be done which would indicate if a regular encoding would be very bad for a particular problem instance and perhaps then encode it in a different way.