velikost textu

Modelling and Solving Problems Using SAT Techniques

Upozornění: Informace získané z popisných dat či souborů uložených v Repozitáři závěrečných prací nemohou být použity k výdělečným účelům nebo vydávány za studijní, vědeckou nebo jinou tvůrčí činnost jiné osoby než autora.
Název:
Modelling and Solving Problems Using SAT Techniques
Typ:
Disertační práce
Autor:
RNDr. Tomáš Balyo
Školitel:
prof. RNDr. Roman Barták, Ph.D.
Oponenti:
doc. Ing. Filip Železný, Ph.D.
Prof. Armin Biere
Konzultant:
RNDr. Pavel Surynek, Ph.D.
Id práce:
84536
Fakulta:
Matematicko-fyzikální fakulta (MFF)
Pracoviště:
Katedra teoretické informatiky a matematické logiky (32-KTIML)
Program studia:
Informatika (P1801)
Obor studia:
Teoretická informatika (4I1)
Přidělovaný titul:
Ph.D.
Datum obhajoby:
29. 9. 2014
Výsledek obhajoby:
Prospěl/a
Jazyk práce:
Angličtina
Klíčová slova:
Splnitelnost, Plánování, Modelování
Klíčová slova v angličtině:
Satisfiability, Planning, Modeling
Abstrakt:
Řešení problémů plánování prostřednictvím překladů do splnitelnosti (SAT) je jedním z nejúspěšnějších přístupů k automatickému plánování. V této práci popíšeme několik způsobů jak přeložit problém plánování reprezentovaný v SAS+ formalismu do SAT. Přezkoumáme a přizpůsobíme stávající kódování a také zavedeme nové vlastní způsoby kódování. Porovnáme jednotlivá kódování pomocí výpočtu horních odhadů na velikosti formulí, které produkují, a pomocí spuštění rozsáhlých experimentů na referenčních problémech z Mezinárodní plánovací soutěže 2011. V experimentální části také porovnáme své kódování s nejmodernejšími kódováními z plánovače Madagascar. Experimenty ukazují, že naše techniky dokažou překonat tato kódování. V předložené práci také řešíme speciální případ optimalizace plánů -- odstranění redundantních akcí. Odstranění všech redundantních akcí je NP- úplný problém. Prostudujeme existující polynomialní heuristické přístupy a navrhneme vlastní heuristický přístup, který dokaže eliminovat vyšší počet a dražší redundantní akce než stávající techniky. Také navrhneme způsob kódování problému redundance plánů do SAT, který nám za použití MaxSAT řešičů umožní optimálně vyřešit problém eliminace redundantních akcí. Naše experimenty provedené s plány od nejmodernejších satisficing plánovačů pro referenční problémy prokázaly, že všechny námi navrhované techniky fungují v praxi velmi dobře. Powered by TCPDF (www.tcpdf.org)
Abstract v angličtině:
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. Powered by TCPDF (www.tcpdf.org)
Dokumenty
Stáhnout Dokument Autor Typ Velikost
Stáhnout Text práce RNDr. Tomáš Balyo 1.02 MB
Stáhnout Abstrakt v českém jazyce RNDr. Tomáš Balyo 84 kB
Stáhnout Abstrakt anglicky RNDr. Tomáš Balyo 84 kB
Stáhnout Posudek vedoucího prof. RNDr. Roman Barták, Ph.D. 93 kB
Stáhnout Posudek oponenta doc. Ing. Filip Železný, Ph.D. 152 kB
Stáhnout Posudek oponenta Prof. Armin Biere 96 kB
Stáhnout Záznam o průběhu obhajoby 201 kB