From: Sandra B Fan (sbfan_at_cs.washington.edu)
Date: Tue Nov 04 2003 - 22:05:54 PST
Title/Author:
"Automatic SAT-Compilation of Planning Problems"
Michael D. Ernest, Todd D. Millstein, and Daniel S. Weld
Summary:
In this paper, the authors outline and test several different methods of
encoding for SAT-compilation.
Most Important Ideas:
This paper provides a useful comparison of how different aspects of
encoding affect performance of the SAT problem. This is important because,
obviously, we are better able to make decisions about what type of
encoding to use.
Secondly, this paper proves that it is possible to automatically compile
encodings for SAT that are on some level comparable to hand-made
encodings, even though it doesn't always beat the hand-made ones. This is
important because it gives us some hope that maybe there's a way
automatic encodings could, in the future, perhaps completely beat
hand-made encodings.
Flaws:
I'm not sure that this is a flaw, but I would have liked to see some
description of the types of problems that these various encodings were run
on and maybe some description of how the type of problem affects the
results.
Open Research Questions:
The authors actually list a large number of interesting future directions.
It would be interesting to find ways to combine different aspects of the
different encodings and see how it affects the results, i.e. try "hybrid"
encodings as mentioned in the paper. Also, another direction could be to
see whether a compiler can generate domain-specific axioms automatically
(though I'm sure it's probably been tried since the publication of this
paper).
This archive was generated by hypermail 2.1.6 : Tue Nov 04 2003 - 22:05:55 PST