Design Automation with SAT-Encoding

Prof. Dan Braha
Ben-Gurion University, Israel

Friday, December 11, 1998
11 a.m.
Fuller Labs 311

In this talk, I will present a computational model for the design process. Design is viewed as a problem-solving process, which attempts to find a concrete artifact that matches a set of functional attributes with a finite sequence of production rules. The computational model is based on representing process states in terms of strings of symbols, and on the effective operations that are built up from very simple manipulations of the strings themselves in the form of production rules.

The computational model will serve as a vehicle for design computer automation. It will also enable us to prove meta-theorems (i.e., theorems about design process properties) related to the correctness, decidability and complexity of design processes. I will show that it is inherently difficult (NP- hard) to identify a sequence of production rules that can be used by the design problem solving process in order to reach a successful solution. This theorem concludes that design problem solving, particularly with its large volume of selection information, requires effective design search procedures.

In this talk, I will suggest a new approach that encodes a design search problem as a propositional satisfiability problem. That is, the problem of finding a truth assignment for propositions that satisfies a set of axioms. A major advantage of the proposed approach is the ability to benefit from recently developed powerful randomized search algorithms for solving non-trivial satisfiability problems that have an order of magnitude larger than can be solved by the most widely-used satisfiability algorithms. The proposed approach provides a flexible framework for stating different kinds of design plan constraints (e.g., de-coupling of a coupled design). The new design-as- satisfiability technique also more accurately reflects the theory behind modern constraint-based design systems, and can greatly enhance current "intelligent" Computer Aided Design tools.

Based on the computational model, I will articulate a descriptive design complexity a la Kolmogorov algorithmic complexity. Finally, I will show that the descriptive complexity measures as applied to product assembly highly correlate over a wide range of experiments with real product assembly times.

Host

David Brown

Colloquium Coordinator

Carolina Ruiz

Maintained by webmaster@wpi.edu
Last modified: Sep 27, 2006, 16:05 EDT