Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving

Many computations over trees can be specified using attribute
grammars. Compilers for attribute grammars need to find an
evaluation order (or schedule) in order to generate efficient code. For the
class of linearly ordered attribute grammars such a schedule can be found
statically, but this problem is known to be NP-hard.
In this paper, we show how to encode linearly ordered attribute grammar
scheduling as a SAT-problem. For such grammars it is necessary to
ensure that the dependency graph is cycle free, which we approach in a
novel way by transforming the dependency graph to a chordal graph allowing
the cycle freeness to be efficiently expressed and computed using
SAT solvers.
There are two main advantages to using a SAT-solver for scheduling:
(1) the scheduling algorithm runs faster than existing scheduling algorithms
on real-world examples, and (2) by adding extra constraints we
obtain fine-grained control over the resulting schedule, thereby enabling
new scheduling optimisations.