Solving combinatorial problems by grounding from specifications

点击翻译按钮获取中文摘要

Challenging combinatorial search and optimization problems are ubiquitous and diverse. A few examples include finding exam timetables, scheduling machines, constructing phylogenetic trees, configuring complex systems, and finding bugs in computer systems. Most of these problems belong to a class of problems (known as the NP-complete problems) for which no known algorithms exist which are guaranteed to be efficient, and moreover, instances that arise in practice often cannot be solved by current methods in reasonable time. They thus present major scientific and practical challenges. The proposed research aims to develop new methods for handling such problems, in particular addressing two issues with the current state-of-the-art in combinatorial problem solving methods. First, while current algorithms and computers are able to easily produce solutions for many problems that workers in many areas face, the technology to do so is not accessible to - or even known to - many of these workers. A primary goal is to develop methods that are much more accessible, in particular by providing modelling languages and software tools which allow complex underlying computational resources to be used by workers who are not specialists in combinatorial problem solving. Second, there remain a number of areas where the best existing combinatorial solving methods do not work effectively or robustly, in spite of the fact that the mainstream technologies are highly developed and based on decades of high quality science. Another goal is to further develop a newer algorithmic approach for solving such problems, and for exploiting computer processors with many cores - which will soon be in standard desktop computers - in the service of solving these problems. In our approach, both modelling languages and computational solving methods are based on an underlying formalization in mathematical logic, which provides a number of benefits in both theoretical and practical work.