Descriptive Complexity measures the richness of a language or sentence needed to describe a given property. There is a profound relationship between the traditional computational complexity of a problem and the descriptive complexity of the problem. In particular, the trade-off between parallel time and amount of hardware, which is a fundamental issue in computation, has been characterized as the trade-off between formula size and number of variables.

Informed by descriptive complexity, PI will use modern SAT solvers, SMT solvers and AI planners to automatically derive efficient algorithms from high-level specifications. PI and his research group will also develop a system that uses solvers to automatically derive low-level reductions between combinatorial problems. Thus methods will be developed to automatically go from high-level specifications to efficient programs as well as to automatically derive lower bounds on how efficient such implementations can be. In using and building these systems, students and established researchers will gain knowledge on what makes problems computationally complex, and how to use state-of-the art solvers to automatically build efficient and reliable software.

Project Start
Project End
Budget Start
2011-09-01
Budget End
2014-08-31
Support Year
Fiscal Year
2011
Total Cost
$341,341
Indirect Cost
Name
University of Massachusetts Amherst
Department
Type
DUNS #
City
Amherst
State
MA
Country
United States
Zip Code
01003