 |
|  |
Programming environment for solving hard optimization problems
University of Kentucky The lack of high-level software tools to support and facilitate the use of automated reasoning technology is a major limiting factor preventing it from realizing its full potential in terms of both performance and acceptance.Automated reasoning of interest in this project is encapsulated by programs called SAT solvers. These programs have been developed to solve computationally hard problems stated in the language of logic. Recent research has demonstrated that SAT solvers are applicable in other domains. They are quickly becoming computationally feasible for applications of critical practical importance in scheduling, planning, combinatorial optimization, electronic design automation, hardware and software verification and many others. At the same time, software tools to support and facilitate the use of SAT solvers are lagging behind. They are ad hoc and problem specific. They constitute a major obstacle that must be addressed in order to take full advantage of the computational potential of the SAT technology, and push the limits of their applicability further. We propose to develop (1) a high-level modeling language for programming search problems, (2) programmer support tools to automate tasks of reasoning about, debugging, rewriting and optimizing problem specifications, and compiling them to SAT formats, (3) tools for integrating SAT programming with other programming environments, (4) new SAT solvers that can be fine-tuned to take advantage of the high-level structure of a problem, and (5) support for user-defined constraints in the modeling language, program processing tools and solvers. This research program will advance SAT technology. It will make using SAT solvers easier and will dramatically expand applications of SAT in industry, academia and military.
|
