Declarative Solving of Computationally Hard Search and Optimization Problems
Computationally hard search and optimization problems are ubiquitous in science, engineering and
business. Examples include drug design, protein folding, phylogeny reconstruction, hardware and
software design, test generation and verification, planning, timetabling, scheduling and on and on. In
rare cases, practical application-specific software exists, but most often development of successful
methods requires hiring specialists, and often significant time and expense, to apply one or more
computational approaches. The goal of our project is to provide another practical technology for
solving these problems, but one which would require considerably less specialized expertise on the
part of the user, thus making technology for solving such problems accessible to a wider variety of
users. In this approach, the user gives a precise specification of their search (or optimization)
problem in a declarative modeling language. A solver then takes this specification, together with an
instance of the problem, and produces a solution to the problem (if there is one). We undertake a
research program of both theoretical development and demonstrating practical feasibility through
system development.
The student will be working in a team which includes two faculty members, two PhD students and
two Masters students on a very active ongoing research project. The main task will be to write
specifications of search and optimization problems in an extension of First-Order (Predicate) Logic,
to develop some benchmarks, run experiments on our system and gather the performance statistics.
The student will have a choice of a more theoretical or a more applied work, depending on their
interests. The result will be used in research papers we plan to publish in first-rate academic
conferences and journals.
