Blanc SIMI 2 - Sciences de l'information, de la matière et de l'ingénierie : Sciences de l’information, simulation

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

Submission summary

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

Project coordination

PHILIPPE JEGOU (Organisme de recherche)

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.



Help of the ANR 501,465 euros
Beginning and duration of the scientific project: - 48 Months

Useful links

Explorez notre base de projets financés



ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter