You are here
» Research » Student research projects » SAT-based Planning Using Split Representations: Quantifying the SeparationSAT-based Planning Using Split Representations: Quantifying the Separation
People
Supervisor
Description
One way to solve an optimisation problem is to solve a series of decision problems. This approach has been studied for a number of decades by the Artificial Intelligence planning community.
Key topics to study here are: (1) what decision problems to solve, and in what order to solve them, and (2) how to represent those problems. This project deals with the latter.
One popular representation of decision problems is in Boolean SAT(isfiability). Your project supervisor was the co-author of a proposal to use a "split" representation of actions in this setting. Although some empirical efficiency gains have been noticed using this representation, a core theoretical question is whether or not this representation yields an exponential separation in the efficiency of a SAT procedure. This is the question that you will try to answer in this research project.
Goals
Develop an analytical demonstration of an exponential separation between atomic and split representations of action dynamics in SAT-based planning, or prove that none exists.
Requirements
A passion for theoretical work and artificial intelligence are both required. This one is not for the faint hearted.
Background Literature
https://users.aalto.fi/~rintanj1/satplan.htm
N. Robinson, C. Gretton, D. Pham, and A. Sattar. SAT-Based Parallel Planning Using a Split Representation of Actions. ICAPS 2009.
J. Rintanen. Planning with SAT, Admissible Heuristics and A*. IJCAI 2011.
J. Huang. Extended clause learning. Artif. Intell. 174(15): 1277-1284, 2010.
Gain
Expereince in academic research.
Strong students should expect a publishable result.
Keywords
Artificial Intelligence, SAT, Automated Planning, Hyper Resolution
