This is a past event
Planning is a fundamental activity, impacting our daily lives in many and varied ways. The planning task consists of selecting a sequence of actions to achieve a specified goal from specified starting conditions. This type of problem arises frequently in many contexts. Consider, for example, holiday planning. Various interleaved elements have to be decided: interesting places to visit, a feasible route between them and convenient places to stay. Those decisions will need to take into account all traveller preferences and respect the budgeting and time requirements. In the quest for efficiency, decades of effort have been invested in creating powerful automated solvers. Albeit AI planning had success in various industrial applications, complex real-world problems sometimes require coordinated reasoning efforts with expressive features such as time, arithmetic or concurrency. Due to this dichotomy, complex challenges still remain unaddressed. Satisfiability Modulo Theories (SMT) solvers generalise SAT solvers by including a rich set of mature and efficient reasoners. This talk will explore how we can use SMT solvers to solve expressive numeric planning problems while being flexible with the user preferences.
- Speaker
- Joan Espasa Arxer
- Venue
- Meston 011