Search is one of the fundamental techniques used by many intelligent software systems. There is a big chasm between the languages that programmers use to describe problems and the encodings that are suitable for solvers to conduct search. This research aims to narrow the gap by designing and implementing algorithms for translating declarative specifications of combinatorial problems into efficient encodings. The intellectual merits are novel frameworks and algorithms for translating planning specifications into sophisticated and efficient tabled logic programs, and cutting-edge algorithms for compiling high-level constraints into SAT (satisfiability) encodings. The project's broader significance and importance are its potential to produce long-lasting, significant economic, educational, and social impact because of the ubiquity of combinatorial problems, and the resulting theory and prototypes that will form the technology which enables future systems to obtain high-quality solutions to a variety of combinatorial problems.
This research will focus on two types of combinatorial problems: AI planning and constraint satisfaction problems solved using SAT. Tabled logic programming has been shown to be a powerful and flexible modeling and solving language for planning problems. Nevertheless, it is an art, not a science, to develop efficient planning models in tabled logic programming. The algorithms designed by this research for translating planning specifications into efficient tabled logic programs will have the following capabilities: (1) convert factored representations of states into structural representations that exploit symmetries; (2) extract domain-dependent control knowledge, such as deterministic actions and partial orders; and (3) learn representation-specific heuristics. Global constraints are an important part of constraint programming. They not only allow easy modeling of many problems, but also enable use of powerful propagation algorithms. SAT encoding algorithms have been proposed for some of the global constraints. Nevertheless, there are no well-established algorithms for encoding global constraints into SAT; many other global constraints, such as graph constraints, have not received much attention despite their usefulness in practical applications. This research will produce algorithms for a comprehensive set of global constraints, and will develop a cutting-edge constraint-solving system based on these algorithms.
