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.
