Author:
Department:
Supervisor:
Reviewer:
Reviewer:
Solving planning problems via translation to satisfiability (SAT) is one of the most successful approaches to automated planning. In this thesis we describe several ways of encoding a planning problem represented in the SAS+ formalism into SAT. We review and adapt existing encoding schemes as well as introduce new original encodings. We compare the encodings by calculating upper bounds on the size of the formulas they produce as well as by running extensive experiments on benchmark problems from the 2011 International Planning Competition (IPC). In the experimental section we also compare our encodings with the state-of-the-art encodings of the planner Madagascar. The experiments show, that our techniques can outperform these state-of-the-art encodings. In the presented thesis we also deal with a special case of post-planning optimization -- elimination of redundant actions. The elimination of all redundant actions is NP-complete. We review the existing polynomial heuristic approaches and propose our own heuristic approach which can eliminate a higher number and more costly redundant actions than the existing techniques. We also propose a SAT encoding for the problem of plan redundancy which together with MaxSAT solvers allows us to solve the problem of action elimination optimally. Experiments done with plans from state-of-the-art satisficing planners for IPC benchmark problems demonstrate, that all the proposed techniques work well in practice.
PhD Thesis Fulltext:
Abstract of Doctoral Thesis:
Resources (sourcecode + data):
Defense Presentaion Slides:
Review - Barták:
Review - Biere:
Review - Železný:
Academic CV:
Professional CV:
Publications by type:
DBLP Publications: