Tractability for Understanding and Pushing forward the Limits of Efficient Solvers – TUPLES

The aim of this project is to significantly push forward the observed effectiveness of resolution systems (called "solvers") while providing the theoretical tools necessary for this purpose. We plan to address this issue through the development and exploitation of tractable classes. This study concerns the field of Artificial Intelligence, specifically the SAT (satisfiability problem in logic) and CSP (Constraint Satisfaction Problem) formalisms. Other closely-related areas of AI, such as planning, will also be studied.

In Complexity Theory, the study of tractable classes is designed to circumvent the difficulty of many problems in computer science (SAT and CSP are NP-complete) by trying to identify sub-problems which can be solved in polynomial time. This question has over a long period led to many developments in different areas. Two important formalisms have emerged in recent decades: SAT and CSP. They have the virtue of being both decidable and sufficiently powerful to express many problems. As they are NP-Complete, two approaches have been adopted to solve them. On the one hand, efficient optimized solvers can often be applied to very large problems from real-world applications. On the other hand, a more theoretical approach restricts the expressiveness of languages for describing problems in order to ensure the existence of efficient (polynomial-time) algorithms, these restrictions defining what are known as tractable classes. Both approaches, although they have produced significant advances, in practice or in theory, still leave many questions unanswered.

Indeed, the tractable classes exhibited are often artificial, in that the conditions guaranteeing tractability are very restrictive (SAT formulas with two literals or CSP on trees, for example). The sub-problems are then of very limited interest. Moreover, there is a real lack of unification of these classes in that, in most cases, their use requires the development of ad-hoc recognition and solving algorithms specific to just one class. This lack of generality is one reason why efficient solvers do not make use of them. In practice, many very large SAT or CSP instances (involving millions of variables) can nevertheless be solved without having recourse to these tractable classes. The power of these systems is generally based on algorithmic techniques such as constraint propagation and/or learning, backed up by extremely effective heuristics. However, despite real successes in practice, the current state of knowledge cannot theoretically explain this observed efficiency, and therefore offers no tool for a priori estimation of the effectiveness of solvers. Furthermore, a plateau appears to have been reached in terms of efficiency. To go beyond this plateau requires fundamentally new ideas.

The aims and ambitions of the project can be summarized in three points:
· To better understand the origins of theoretical tractability and the reasons for the practical effectiveness of the solvers (based on theoretical criteria of tractability)
· To develop new tractable classes that would capture the essential qualities of many real problem instances and be both effective and easy to implement
· Significantly extend the capabilities of current solvers to a new level by incorporating the exploitation of tractable classes