Student research opportunities

Stochastic Local Search for SAT Encodings of Planning Problems

Project Code: CECS_814

This project is available at the following levels:
CS single semester, Engn4200, Honours, Summer Scholar, Masters, PhD

Keywords:

Boolean Satisfiability, Local Search, Clause Learning

Supervisors:

Dr Charles GRETTON
Dr Phil Kilby
Dr Patrik Haslum

Outline:

Automated planning is a subfield of artificial intelligence that
studies the problem of synthesizing action strategies that enable
artificially intelligent systems to achieve their goals and
objectives. In this project, the student will study and develop a
planning system for the case where action strategies correspond to
discrete sequences of actions. Such systems have applications in
elevator scheduling, logistical problems, chemical plant control,
orbital observation scheduling, AI player control in computer gaming,
and planetary-rover control.

One of the most powerful and general technologies to arise from
research in Artificial Intelligence and Automated Reasoning is
efficient search. This project shall focus in particular on
search-based solution procedures for Boolean Satisfiability (SAT)
problems. Indeed, the most efficient and scalable procedures for
finding short plans are SAT-based. SAT-based procedures are also the
most scalable and efficient at planning under tight time constraints.
Currently the best procedures in this vein employ what is broadly
known to be a "backtracking" search. There is however strong evidence
that for many problems a more efficient approach would be to use a "local"
search. The purpose of this project is to develop and explore local
search techniques for SAT-based planning.

Goals of this project

Research, develop and explore local search techniques for SAT-based planning.

There are many interesting topics to study in this direction. These comprise scientific questions that can be resolved in the short term, for example exploring analogues of clause-learning in local search, to much more difficult questions in the domain of representation and heuristics. The latter would be appropriate to study for an advanced honours thesis. The former can be studied as part of a summer project.

(Higher Degree -- PhD) There are very significant research questions (both theoretical and empirical) in this direction that can underlie an ambitious higher degree project. Please contact/write-to me if this interests you, and I can provide further details.

Requirements/Prerequisites

Ambitious hard working student with a strong track record in technical subjects.

Must have a passion for automating reasoning.

The student who undertakes this project should wish to pursue a
research career in Computer Science. Either as a research engineer, or academic.

If in doubt, _please_ write to us...

Student Gain

Experience working at NICTA, a world-class ITC research organisation.

Graduate level knowledge of key topics in Automated Reasoning and Artificial Intelligence.

Background Literature

Jussi Rintanen: Planning with Specialized SAT Solvers. AAAI 2011.

Silvia Richter and Matthias Westphal. The LAMA Planner: Guiding
Cost-Based Anytime Planning with Landmarks. Journal of Artificial
Intelligence Research (JAIR) 39, pp. 127-177, 2010.

Nathan Robinson, Charles Gretton, Duc Nghia Pham, Abdul Sattar:
Partial Weighted MaxSAT for Optimal Planning. PRICAI 2010: 231-243.

Nathan Robinson, Charles Gretton, Duc Nghia Pham, Abdul Sattar:
SAT-Based Parallel Planning Using a Split Representation of
Actions. ICAPS 2009.

Duc Nghia Pham, John Thornton, Charles Gretton, Abdul Sattar:
Combining Adaptive and Dynamic Local Search for Satisfiability. JSAT
4(2-4): 149-172 (2008).