Offre de postdoc et th
Forum 'Emplois' - Sujet créé le 2011-07-06 par Pierre Lopez
====POSTDOC=====
We are seeking applicants for a one year postdoc position at LAAS in Toulouse on a collaborative project with the Centre National d'Etudes Spatiales (CNES) on scheduling maneuvers and scientific experiments of the Rosetta/Philae spacecraft. Rosetta is a mission of the European Space Agency (ESA) and will involve the first ever landing on a Comet (67P / Churyumov - Gerasimenko) http://sci.esa.int/science-e/www/area/index.cfm?fareaid=13. The postdoc will start at the earliest in September 2011, and at the latest in January 2012.
=========== PROJECT ============
The project is concerned with developing algorithms for scheduling the various activities of the lander (Philae) in three phases. First, in the Separation, Descent and Landing (SDL) phase, the lander will be separated from the orbiter module and will land on the surface of the comet. Second, during the First Science Sequence (FSS), the main scientific experiments will be run using the onboard batteries as energy source. This phase should last three to four days, depending on the load of the batteries and on the quality of the schedule. Finally, during the Long Term Science phase, scientific activities will be resumed at a much slower pace, using the lander's own solar panels to partially reload the batteries.
The experiments of the FSS and LTS -- and to some extent the maneuvers of the SDL -- need to be scheduled to satisfy a number of constraints involving the concurrent use of energy (batteries), and of the main CPUs as well as each instrument's memory. Another important constraint concerns the transfer of data and the notion of "visibility", that is, the availability of the orbiter to act as relay to transmit the data back to earth, which depends on its orbit and on the length of a cometal day. A tool developed using Ilog Scheduler and Solver (MOST) is currently used to model this problem and to generate feasible plans. Every instrument, subsystem and experiment has been modeled with this library, and it is therefore possible to verify solutions with a great degree of confidence of its feasibility. However, the complexity of the problem, in particular during the FSS phase, makes it difficult to find solutions in a reasonable time.
The role of the recruited researcher will be to explore ways of obtaining better solutions quicker, and to develop prototypes to assess the gain. This might be done by improving the model, the propagation algorithms and the search strategies currently employed, or by developing radically new models whose solutions can then be fed back to MOST.
=========== WORKING ENVIRONMENT ============
The project is expected to be carried out in collaboration with Pierre Lopez, Christian Artigues and Emmanuel Hebrard (MOGISA group: http://www.laas.fr/MOGISA-EN/), and in constant contact with the SONC team (http://smsc.cnes.fr/ROSETTA/GP_contacts.htm) of the CNES.
=========== APPLICATION ============
We are seeking applicants with an outstanding cv and a thesis related to scheduling and/or combinatorial optimization. A good experience of IBM/Ilog products would be a great plus, however it is not necessary.
Please send the following documents to Emmanuel Hebrard (hebrard@laas.fr) straightaway:
- A detailed curriculum vitae;
- A motivation letter;
- Abstract of the PhD thesis;
- The three most relevant publications;
- (optional) Reference letters from at most three referees.
====THESIS====
*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)
We are seeking applicants for a one year postdoc position at LAAS in Toulouse on a collaborative project with the Centre National d'Etudes Spatiales (CNES) on scheduling maneuvers and scientific experiments of the Rosetta/Philae spacecraft. Rosetta is a mission of the European Space Agency (ESA) and will involve the first ever landing on a Comet (67P / Churyumov - Gerasimenko) http://sci.esa.int/science-e/www/area/index.cfm?fareaid=13. The postdoc will start at the earliest in September 2011, and at the latest in January 2012.
=========== PROJECT ============
The project is concerned with developing algorithms for scheduling the various activities of the lander (Philae) in three phases. First, in the Separation, Descent and Landing (SDL) phase, the lander will be separated from the orbiter module and will land on the surface of the comet. Second, during the First Science Sequence (FSS), the main scientific experiments will be run using the onboard batteries as energy source. This phase should last three to four days, depending on the load of the batteries and on the quality of the schedule. Finally, during the Long Term Science phase, scientific activities will be resumed at a much slower pace, using the lander's own solar panels to partially reload the batteries.
The experiments of the FSS and LTS -- and to some extent the maneuvers of the SDL -- need to be scheduled to satisfy a number of constraints involving the concurrent use of energy (batteries), and of the main CPUs as well as each instrument's memory. Another important constraint concerns the transfer of data and the notion of "visibility", that is, the availability of the orbiter to act as relay to transmit the data back to earth, which depends on its orbit and on the length of a cometal day. A tool developed using Ilog Scheduler and Solver (MOST) is currently used to model this problem and to generate feasible plans. Every instrument, subsystem and experiment has been modeled with this library, and it is therefore possible to verify solutions with a great degree of confidence of its feasibility. However, the complexity of the problem, in particular during the FSS phase, makes it difficult to find solutions in a reasonable time.
The role of the recruited researcher will be to explore ways of obtaining better solutions quicker, and to develop prototypes to assess the gain. This might be done by improving the model, the propagation algorithms and the search strategies currently employed, or by developing radically new models whose solutions can then be fed back to MOST.
=========== WORKING ENVIRONMENT ============
The project is expected to be carried out in collaboration with Pierre Lopez, Christian Artigues and Emmanuel Hebrard (MOGISA group: http://www.laas.fr/MOGISA-EN/), and in constant contact with the SONC team (http://smsc.cnes.fr/ROSETTA/GP_contacts.htm) of the CNES.
=========== APPLICATION ============
We are seeking applicants with an outstanding cv and a thesis related to scheduling and/or combinatorial optimization. A good experience of IBM/Ilog products would be a great plus, however it is not necessary.
Please send the following documents to Emmanuel Hebrard (hebrard@laas.fr) straightaway:
- A detailed curriculum vitae;
- A motivation letter;
- Abstract of the PhD thesis;
- The three most relevant publications;
- (optional) Reference letters from at most three referees.
====THESIS====
*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)