Review: Automatic SAT-Compilation

From: Julie Letchner (letchner_at_cs.washington.edu)
Date: Wed Nov 05 2003 - 03:20:01 PST

  • Next message: Danny Wyatt: "Automatic SAT-compilation"

    The authors present a 2D space of STRIPS-to-SAT encodings/transformations,
    and develop optimizations to make automation of these transformations more
    effective. Experimental results from their MEDIC compiler are presented on
    8 encodings to support conclusions about the effectiveness of
    these transformations and how they are influenced by optimizations.

    The first major idea in this paper is that the space of
    planning-to-satisfiability problem transformations can be described on a
    set of axes. This idea immediately invites experiments that can extract
    high-level behaviors and tradeoffs between encodings in different regions
    of the transformation space. Indeed this paper performs some of these
    experiments, and gives a preliminary partial ordering on regions in the
    space based upon their effectiveness; this partial ordering is useful for
    focusing future work on areas likely to produce the best results.

    The second major idea in this paper is that the transformations described
    by the aforementioned 2D space can be effectively automated. Optimizations
    are the key here, and the authors detail some of their own; however, I
    think the more important contribution is that they show results positive
    enough to motivate future work on optimizations, as well as providing
    reasoned discussion to guide this future work.

    The largest flaw with this paper is that with the exception of the
    high-level identification of the best and worst encodings, it is difficult
    to pull meaningful information from its evaluation section. I would have
    liked to see a graph showing overall trends, and the major graph in the
    Experiments section (Figure 6) is disappointing. In trying to convey too
    much information it makes the task of tracing the data for any single
    encoding exceedingly difficultnot to mention that the x-axis labels
    relating the names of the STRIPS scheme are useless, since nowhere in the
    paper is the reader given any characteristics of these varying schemata. I
    think this figure would have been more effective if it presented
    aggregates, and a fuller evaluation would have given the relative rankings
    of all the encodings for each of the performance metrics used.

    The murkiness of the evaluation section suggests that useful future work
    may include a methodology for evaluation of these encodings; in particular,
    some relationship pulling together #variables, #clauses, and #literals into
    some notion of utility would be useful. On a brighter note, this paper
    makes it clear that further work on optimized compilers will be useful, and
    it provides a solid starting point for that work.

    ~*~*~*~*~*~*~*~*~*~*~
    Julie Letchner
    (206) 890-8733
    University of Washington
    Computer Science & Engineering
    letchner_at_cs.washington.edu


  • Next message: Danny Wyatt: "Automatic SAT-compilation"

    This archive was generated by hypermail 2.1.6 : Wed Nov 05 2003 - 03:20:35 PST