Knowledge compilation for incorporating constraints

This dissertation defines knowledge compilation as the transformation of a design task's declarative specification into an algorithm that performs the task and effectively incorporates the task's knowledge. The specification describes the task to be performed without prescribing a method for performing it. This dissertation presents a method (implemented in the RICK program) that automatically refines a task specification into synthesis knowledge encoded as constrained generators. These generators exhaustively enumerate solutions satisfying this specification without using testers.;RICK compiles specifications for spatial configuration tasks defining an artifact whose parts must be placed and oriented either geometrically or topologically to satisfy a set of constraints on the artifact's structure. Constrained generators incorporate the knowledge for synthesizing the artifact including many of its structural constraints. The remaining constraints represent analysis knowledge that is used to test a solution's acceptability.;Other approaches have tried to incorporate this analysis knowledge after creating a generation algorithm. These approaches do not avoid the potential mismatch between the structure of the generation algorithm and the structure of the constraints (the structure mismatch problem). RICK refines a task's analysis knowledge into a generation algorithm and uses the task's constraints to define the representation of the artifact to avoid this mismatch. As a result of this refinement, the structure of the generation algorithm corresponds to the solution structure defined by the constraints. With this correspondence, the analysis knowledge can be incorporated into the generation algorithm, making it a constrained generator.;By focusing on spatial configuration tasks, including many practical problems such as VLSI layout and architecture design, particular properties of these tasks allow RICK to automatically synthesize constrained generators. Viewed as a contribution to automatic software design, RICK's method compiles a task specification expressed at a more abstract, more declarative level than other software design methods.