Using Constrained Horn Clauses for Hierarchical Planning
| Název práce v češtině: | Užití omezených Hornových klauzulí pro hierarchické plánování |
|---|---|
| Název v anglickém jazyce: | Using Constrained Horn Clauses for Hierarchical Planning |
| Klíčová slova: | hierarchické plánování|omezené Hornove klauzule|Plánovací problém|Řešič|Tranzitní systém |
| Klíčová slova anglicky: | hierarchical planning|constrained Horn clauses|Planning problem|Solver|Transition system |
| Akademický rok vypsání: | 2020/2021 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | Mgr. Martin Blicha, Ph.D. |
| Řešitel: | Bc. Marián Kažimír - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 28.01.2021 |
| Datum zadání: | 29.01.2021 |
| Datum potvrzení stud. oddělením: | 11.03.2021 |
| Datum a čas obhajoby: | 10.09.2021 09:00 |
| Datum odevzdání elektronické podoby: | 21.07.2021 |
| Datum odevzdání tištěné podoby: | 22.07.2021 |
| Datum proběhlé obhajoby: | 10.09.2021 |
| Oponenti: | Mgr. Kristýna Pantůčková |
| Zásady pro vypracování |
| In classical planning (CP), finding a plan means finding a sequence of actions that lead from an initial state to a goal state, when the actions fully describe in which states they are executable and what effects they have on the world.
Hierarchical planning (HP) extends classical planning by supporting two kinds of tasks: primitive (corresponding to actions in CP) and compound (or abstract) ones. Hierarchical planning has recently seen a renewal of interest in the planning community due to larger expressive power over classical planning. Reduction (or compilation) to SAT and leveraging the recent advances in SAT solving have been successfully applied to both classical and hierarchical planning. Constrained Horn Clauses (CHC) has recently emerged as an intermediate language for expressing verification conditions in software verification. They extend the classical formats for SAT and SMT by capturing high-level constructs such as loops and recursion in low-level logical representation. The state-of-the-art dedicated CHC solvers employ powerful algorithms to detect reachability of error states in the system. The format of CHC is powerful enough to capture the hierarchical structure of HP problems, and the reachability algorithms in CHC solvers can be used to find corresponding plans. The aim of this thesis is to investigate possible compilation techniques of HP to CHC, i.e., propose an encoding of totally-ordered HP problems into CHC, use off-the-shelf CHC solver to solve the compiled problem and extract the plan from the CHC solution. The compilation technique will be implemented and its performance evaluated on a suitable subset of benchmarks from International Planning Competition 2020. |
| Seznam odborné literatury |
| 1. A Survey on Hierarchical Planning – One Abstract Idea, Many Concrete Realizations; Pascal Bercher, Ron Alford, Daniel Höller; IJCAI 2019, https://www.ijcai.org/Proceedings/2019/875
2. HDDL: An Extension to PDDL for Expressing Hierarchical Planning Problems; Daniel Höller, Gregor Behnke, Pascal Bercher, Susanne Biundo, Humbert Fiorino, Damien Pellier, Ron Alford; https://doi.org/10.1609/aaai.v34i06.6542 3. IPC 2020 benchmarks: https://github.com/panda-planner-dev/ipc2020-domains 4. On recursion-free Horn clauses and Craig interpolation; Philipp Rummer, Hossein Hojjat, Viktor Kuncak; https://infoscience.epfl.ch/record/213898 5. Efficient SAT Encodings for Hierarchical Planning; Dominik Schreiber, Damien Pellier, Humbert Fiorino, Tomáš Balyo; ICAART 2019, https://www.scitepress.org/Link.aspx?doi=10.5220/0007343305310538 |