Exploiting constraints in design synthesis

Abstract

The class of design synthesis problems encompasses a wide spectrum of common encountered problems, including robot planning problems, synthesis of electronic circuits, chemical synthesis, genetics experiment design, and computer program synthesis. This thesis is in two main parts, both dealing with design synthesis. The first part is the Residue Method, an abductive approach to design synthesis, and the second is supersumption, a generalization of consistency checking of partially completed designs. The Residue Method synthesizes designs by reduction of the design goal to another, primitively achievable goal. The reduced goal must be consistent with known facts about the world, must be sufficient to achieve the original goal, and must be a conjunction of formulas from a language of primitively achievable formulas. The Residue Method expresses the design goal, the final design, and all intermediate designs as formulas of first order logic. The usual approach in deductive synthesis has been to express designs as a single term of composed state transformation functions. Expression of designs as a formula rather than a term simplifies synthesis of non-linear plans, allows postponing imposition of ordering constraints, and allows one to reason directly about the proposed design. Soundness and completeness results are given for two resolution-based residue procedures. Supersumption is an attempt to exploit the consistency requirement in order to accelerate synthesis of designs. Not only is consistency of a partially completed design checked, but additional may be derived that must be true for the partial design to remain consistent. By making sure that the ramifications are not violated, one avoids searching parts of the search space that do not contain legal designs. In addition, knowing ramifications may make additional search control heuristics directly applicable. The process of imposing additional constraints on a subgoal is called supersumption. Two phenomena are described by which supersumption can speed up the search--use of ramifications as better generators of candidates than the unadorned goal, and use of ramifications as filters to quickly eliminate inconsistent designs. Two resolution-based methods for deriving ramifications are given, along with soundness and completeness results.