Student research opportunities
Expressive Planning via Satisfiability Modulo Theory (several projects inside)
Project Code: CECS_1168
This project is available at the following levels:
CS single semester, Honours, Summer Scholar, Masters
Keywords:
Automated Planning, Satisfiability Modulo Theory, Planning with Expressive Models
Supervisor:
Dr Enrico ScalaOutline:
Planning is the problem of finding a course of actions whose execution leads the agent into a state satisfying a set of goals, while assuring that such actions are actually feasible all along the entailed trajectory of states. In Artificial Intelligence the problem has been tackled from a knowledge representation point view; the purpose is to provide a declarative/model based framework for a general form of reasoning which is actually independent from the specific domain of application but effective enough to obtain success in many application areas (http://sig-aps.org/). To capture interesting real world problems, planning model and languages such as PDDL 3.0 [1] have been developed and a lot of expressiveness has been introduced to reason considering a number of aspects such as qualitative and quantitative conditions, causal and temporal reasoning, local and global constraints. Lots of research has been done to handle very restricted forms of such formulations (e.g., atomic actions, discrete variables and so forth) so challenges still remain open to handle the entire expressiveness, above all when the number of direct and indirect implications entailed by the selection of particular set of actions is not negligible.
Satifiability Modulo Theory is an extension of SAT which allows to express and reason over (mainly quantifier free) sat formulas intertwined with theories such as the one of real and integer numbers ([2]). The satisfiability of a formula depends on finding an interpretation of the variables (i.e. a model) that satisfies the logical and numerical connectives. There have been many advances in the SMT community and powerful solvers have been developed such as MathSat [8] and Z3 [7].
Grounding on current planning via SAT methodologies (see [5]), the scope of this project is to investigate tighter integration between planning and SMT. There are many things that can be investigated in this context, depending on the particular interest of the student/effort, the focus (theoretical, practical, both) and the time at disposal. To name a few of them:
- Extension of classical sat based encoding. The idea is to handle/exploit the SMT expressiveness to implement novel encodings for the planning problems at hand, and to study their impact
- New variable/value orderings heuristics. The idea is to inject planning knowledge (e.g., heuristics as in [3]) within the SMT formulation. This knowledge should focus the resolution towards the actually interesting portions of the search space (the ones actually important and crucial for the problem at hand).
- Comparing SMT planning with State Space Search numeric planners (e.g. [3],[4])
- SMT planning with disjunctive global constraints (case study: navigation with obstacles!)
- SMT formulations accounting actions with (explicit) duration and impact on the cost formulated as criterion that needs to be optimized.
We are also investigating the possibility of applying such methodology for the management of energy systems (http://org.nicta.com.au/portfolio/energy-systems/) and logistic problems (http://org.nicta.com.au/portfolio/logistics-supply-chains-and-transportation/). Domain independent planning trades efficiency for clarity and will be never as efficient as an ad-hoc solution to the problem can be. On the other hand, a domain independent approach offers an extremely high level interface to the problem. The scope is hence to understand and evaluate the actual cost/benefit in terms of performances such as plan generation time and quality of the obtained solution.
Requirements/Prerequisites
Artificial Intelligence course, principles of automated planning, SAT and logic, some basic mathematical background, programming languages such as C++ and/or JAVA.
Background Literature
[1] Fox, Maria, and Derek Long. "PDDL2. 1: An Extension to PDDL for Expressing Temporal Planning Domains." J. Artif. Intell. Res.(JAIR) 20 (2003): 61-124.
[2] Barrett, Clark W., et al. "Satisfiability Modulo Theories." Handbook of satisfiability 185 (2009): 825-885.
[3] Hoffmann, Jörg. "The Metric-FF Planning System: Translating``Ignoring Delete Lists''to Numeric State Variables." Journal of Artificial Intelligence Research (2003): 291-341.
[4] Coles, Amanda Jane, et al. "COLIN: Planning with continuous linear numeric change." Journal of Artificial Intelligence Research (2012): 1-96.
[5] Rintanen, Jussi, Keijo Heljanko, and Ilkka Niemelä. "Planning as satisfiability: parallel plans and algorithms for plan search." Artificial Intelligence 170.12 (2006): 1031-1080.
[6] Rankooh, Masood Feyzbakhsh, and Gholamreza Ghassem-Sani. "New Encoding Methods for SAT-Based Temporal Planning." ICAPS. 2013.
[7] De Moura, Leonardo, and Nikolaj Bjørner. "Z3: An efficient SMT solver." Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2008. 337-340.
[8] Bruttomesso, Roberto, et al. "The mathsat 4 smt solver." Computer Aided Verification. Springer Berlin Heidelberg, 2008.
