Efficient encoding for exact symbolic automata-based scheduling

This paper presents an efficient encoding and automaton construction which improves performance of automata-based scheduling techniques. The encoding preserves knowledge of what operations occurred previously but excludes when they occurred, allowing greater sharing among scheduling traces. The technique inherits all of the features of BDD-based control dominated scheduling including systematic speculation. Without conventional pruning, all schedules for several large samples are quickly constructed.