Autor:
Katedra:
Školitel:
Oponent:
Oponent:
Ř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.
Text disertační práce:
Autoreferát:
Příloha (zdrojové kódy + data):
Prezentace k obhajobě:
Posudek - Barták:
Posudek - Biere:
Posudek- Železný:
Akademický životopis:
Profesionální životopis:
Publikace dle typu:
DBLP Publikace: