# Offre de th

Forum 'Annonces' - Sujet créé le 2011-07-06
par
**Pierre Lopez**

*Thesis proposal* :

Satisfiability Modulo Theories for Scheduling

*General context* :

This thesis topic is part of a CNRS-Google project and will be hosted in a French laboratory in Toulouse: LAAS (http://www.laas.fr).

*Contacts* :

Emmanuel Hebrard: emmanuel.hebrard@laas.fr

Christian Artigues: christian.artigues@laas.fr

Pierre Lopez: pierre.lopez@laas.fr

*Abstract* :

The objective is to develop a new framework inspired from the Satisfiability Modulo Theories framework for solving scheduling problems. The main idea is to emulate the key features of satisfiability solvers - clause learning and conflict directed backjumping - whilst providing data structures and inference mechanisms from linear and constraint programming, hence adapted to temporal problems.

*Description* :

Scheduling has been a rich application domain for a number of combinatorial optimization paradigms. Integer Linear Programming (ILP), Constraint Programming (CP), and Metaheuristics have all yielded successful methods for these problems. Recently, however, approaches inspired by the Boolean Satisfiability (SAT) world have been proven to be extremely successful for a wide range of scheduling problems [1][2]. The key-feature of these methods is to learn, during search, new clauses corresponding to inconsistent sub-problems. Adding these newly learnt clauses progressively tightens the model and therefore reduces the search space.

However, there is currently no method for resource scheduling that takes full advantage of SAT-based conflict analysis while using dedicated data structures and dedicated algorithms for reasoning about resource and temporal constraints. Indeed, the methods introduced in [3] and [4] require discretizing the time horizon, which is often impractical. On the other hand, the approach used in [5] only learns a very restricted form of clauses and do not use them to backjump.

Satisfiability Modulo Theories (SMTs) is a framework that precisely allows the association of various domain specific algorithms (denoted theories) with a SAT-based search procedure [6].

In this PhD, we propose to study Sat Modulo Theories as framework to solve scheduling problems. The "scheduling theory" will encapsulate known constraint programming methods. A first important venue of research is to develop new filtering algorithms or to improve existing ones for global constraints corresponding to recurring patterns in scheduling problems. See for instance [7] for this type of results on a global filtering procedure for problems with maximum time-lag constraints, or [8] for problems with cumulative resources and non-uniform consumption. A second important problem is to compute "explanations" of inconsistent states, or of domain reductions due to the constraints. Indeed, these explanations are the central element of communication between the theory (constraint programming part) and the Boolean Satisfiability search algorithm. Computing short explanations efficiently is therefore critical to the overall efficiency of the system.

*Required skills* :

Applicants should have an outstanding academic record and a bachelor-level degree in computer science. They should have good programming skills, an interest as well as a good understanding of Combinatorial Optimization, and should be knowledgeable in at least some of the methods that will be investigated: Constraint Programming, Boolean Satisfiability, Integer Programming, and Satisfiability Modulo Theories. Prior knowledge of French is a plus though not mandatory.

*Working environment* :

The student will work on this project in collaboration with Emmanuel Hebrard, Christian Artigues, and Pierre Lopez, and more generally with members of the MOGISA group (http://www.laas.fr/MOGISA-EN/) at LAAS. The scientific activities of the group are focused on scheduling, transportation, discrete optimization, and constraint satisfaction.

This project is in collaboration with Google, however it is not an industrial project. In other words, there are no precise deliverables, and the student is on the contrary encouraged to develop is own original research path. In particular, we aim at balancing theoretical (algorithm design, complexity analysis, etc.) and applied research, the focus will depend on the preferences and skills of the student.

The PhD is partly funded by the "Région Midi-Pyrénées".

*Expected starting date for the PhD* :

October-November 2011

*Application process* :

Please send the following documents to Emmanuel Hebrard (hebrard@laas.fr) straightaway:

- A detailed curriculum vitae;

- The results and ranking in the last two years of academic studies;

- A motivation letter;

- (optional) Reference letters from at most three referees.

Selected candidates are expected to be interviewed (in the lab or by visioconference).

*Bibliography* :

[1] J. Coelho and M. Vanhoucke. Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers. European Journal of Operational Research, 213(1):73-82, 2011.

[2] A. Horbach. A Boolean satisfiability approach to the resource-constrained project scheduling problem. Annals of Operations Research, 181:89–107, 2010.

[3] N. Tamura, A. Taga, S. Kitagawa, and M. Banbara. Compiling Finite Linear CSP into SAT. In Frédéric Benhamou, editor, Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming (CP-06), pages 590–603, Nantes, France, 2006.

[4] T. Feydy and P. J. Stuckey. Lazy Clause Generation Reengineered. In Ian Gent, editor, Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming (CP- 09), Lecture Notes in Computer Science, pages 352–366, Lisbon, Portugal, September 2009. Springer-Verlag.

[5] D. Grimes, E. Hebrard, and A. Malapert. Closing the Open Shop: Contradicting Conventional Wisdom. In Ian Gent, editor, Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming (CP-09), Lecture Notes in Computer Science, pages 400–408, Lisbon, Portugal, September 2009. Springer-Verlag.

[6] R. Nieuwenhuis, A. Oliveras, and C. Tinelli. 2006. Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53, 6 (November 2006), 937-977.

[7] C. Artigues, M.-J. Huguet, and P. Lopez. Generalized Disjunctive Constraint Propagation for Solving the Job Shop Problem with Time Lags. Engineering Applications of Artificial Intelligence, 24(2):220-231, 2011.

[8] C. Artigues, P. Lopez, and A. Haït. The energy scheduling problem: Industrial case-study and constraint propagation techniques. International Journal of Production Economics, to appear.

Satisfiability Modulo Theories for Scheduling

*General context* :

This thesis topic is part of a CNRS-Google project and will be hosted in a French laboratory in Toulouse: LAAS (http://www.laas.fr).

*Contacts* :

Emmanuel Hebrard: emmanuel.hebrard@laas.fr

Christian Artigues: christian.artigues@laas.fr

Pierre Lopez: pierre.lopez@laas.fr

*Abstract* :

The objective is to develop a new framework inspired from the Satisfiability Modulo Theories framework for solving scheduling problems. The main idea is to emulate the key features of satisfiability solvers - clause learning and conflict directed backjumping - whilst providing data structures and inference mechanisms from linear and constraint programming, hence adapted to temporal problems.

*Description* :

Scheduling has been a rich application domain for a number of combinatorial optimization paradigms. Integer Linear Programming (ILP), Constraint Programming (CP), and Metaheuristics have all yielded successful methods for these problems. Recently, however, approaches inspired by the Boolean Satisfiability (SAT) world have been proven to be extremely successful for a wide range of scheduling problems [1][2]. The key-feature of these methods is to learn, during search, new clauses corresponding to inconsistent sub-problems. Adding these newly learnt clauses progressively tightens the model and therefore reduces the search space.

However, there is currently no method for resource scheduling that takes full advantage of SAT-based conflict analysis while using dedicated data structures and dedicated algorithms for reasoning about resource and temporal constraints. Indeed, the methods introduced in [3] and [4] require discretizing the time horizon, which is often impractical. On the other hand, the approach used in [5] only learns a very restricted form of clauses and do not use them to backjump.

Satisfiability Modulo Theories (SMTs) is a framework that precisely allows the association of various domain specific algorithms (denoted theories) with a SAT-based search procedure [6].

In this PhD, we propose to study Sat Modulo Theories as framework to solve scheduling problems. The "scheduling theory" will encapsulate known constraint programming methods. A first important venue of research is to develop new filtering algorithms or to improve existing ones for global constraints corresponding to recurring patterns in scheduling problems. See for instance [7] for this type of results on a global filtering procedure for problems with maximum time-lag constraints, or [8] for problems with cumulative resources and non-uniform consumption. A second important problem is to compute "explanations" of inconsistent states, or of domain reductions due to the constraints. Indeed, these explanations are the central element of communication between the theory (constraint programming part) and the Boolean Satisfiability search algorithm. Computing short explanations efficiently is therefore critical to the overall efficiency of the system.

*Required skills* :

Applicants should have an outstanding academic record and a bachelor-level degree in computer science. They should have good programming skills, an interest as well as a good understanding of Combinatorial Optimization, and should be knowledgeable in at least some of the methods that will be investigated: Constraint Programming, Boolean Satisfiability, Integer Programming, and Satisfiability Modulo Theories. Prior knowledge of French is a plus though not mandatory.

*Working environment* :

The student will work on this project in collaboration with Emmanuel Hebrard, Christian Artigues, and Pierre Lopez, and more generally with members of the MOGISA group (http://www.laas.fr/MOGISA-EN/) at LAAS. The scientific activities of the group are focused on scheduling, transportation, discrete optimization, and constraint satisfaction.

This project is in collaboration with Google, however it is not an industrial project. In other words, there are no precise deliverables, and the student is on the contrary encouraged to develop is own original research path. In particular, we aim at balancing theoretical (algorithm design, complexity analysis, etc.) and applied research, the focus will depend on the preferences and skills of the student.

The PhD is partly funded by the "Région Midi-Pyrénées".

*Expected starting date for the PhD* :

October-November 2011

*Application process* :

Please send the following documents to Emmanuel Hebrard (hebrard@laas.fr) straightaway:

- A detailed curriculum vitae;

- The results and ranking in the last two years of academic studies;

- A motivation letter;

- (optional) Reference letters from at most three referees.

Selected candidates are expected to be interviewed (in the lab or by visioconference).

*Bibliography* :

[1] J. Coelho and M. Vanhoucke. Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers. European Journal of Operational Research, 213(1):73-82, 2011.

[2] A. Horbach. A Boolean satisfiability approach to the resource-constrained project scheduling problem. Annals of Operations Research, 181:89–107, 2010.

[3] N. Tamura, A. Taga, S. Kitagawa, and M. Banbara. Compiling Finite Linear CSP into SAT. In Frédéric Benhamou, editor, Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming (CP-06), pages 590–603, Nantes, France, 2006.

[4] T. Feydy and P. J. Stuckey. Lazy Clause Generation Reengineered. In Ian Gent, editor, Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming (CP- 09), Lecture Notes in Computer Science, pages 352–366, Lisbon, Portugal, September 2009. Springer-Verlag.

[5] D. Grimes, E. Hebrard, and A. Malapert. Closing the Open Shop: Contradicting Conventional Wisdom. In Ian Gent, editor, Proceedings of the 15th International Conference on Principles and Practice of Constraint Programming (CP-09), Lecture Notes in Computer Science, pages 400–408, Lisbon, Portugal, September 2009. Springer-Verlag.

[6] R. Nieuwenhuis, A. Oliveras, and C. Tinelli. 2006. Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53, 6 (November 2006), 937-977.

[7] C. Artigues, M.-J. Huguet, and P. Lopez. Generalized Disjunctive Constraint Propagation for Solving the Job Shop Problem with Time Lags. Engineering Applications of Artificial Intelligence, 24(2):220-231, 2011.

[8] C. Artigues, P. Lopez, and A. Haït. The energy scheduling problem: Industrial case-study and constraint propagation techniques. International Journal of Production Economics, to appear.