Property Directed Reachability for Automated Planning

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F14%3A10283342" target="_blank" >RIV/00216208:11320/14:10283342 - isvavai.cz</a>

Výsledek na webu

<a href="http://jair.org/media/4231/live-4231-7958-jair.pdf" target="_blank" >http://jair.org/media/4231/live-4231-7958-jair.pdf</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1613/jair.4231" target="_blank" >10.1613/jair.4231</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Property Directed Reachability for Automated Planning

Popis výsledku v původním jazyce

Property Directed Reachability (PDR) is a very promising recent method for deciding reachability in symbolically represented transition systems. While originally conceived as a model checking algorithm for hardware circuits, it has already been successfully applied in several other areas. This paper is the first investigation of PDR from the perspective of automated planning. Similarly to the planning as satisfiability paradigm, PDR draws its strength from internally employing an efficient SAT-solver. We show that most standard encoding schemes of planning into SAT can be directly used to turn PDR into a planning algorithm. As a non-obvious alternative, we propose to replace the SAT-solver inside PDR by a planningspecific procedure implementing the same interface. This SAT-solver free variant is not only more efficient, but offers additional insights and opportunities for further improvements. An experimental comparison to the state of the art planners finds it highly competitive, solv

Název v anglickém jazyce

Property Directed Reachability for Automated Planning

Popis výsledku anglicky

Property Directed Reachability (PDR) is a very promising recent method for deciding reachability in symbolically represented transition systems. While originally conceived as a model checking algorithm for hardware circuits, it has already been successfully applied in several other areas. This paper is the first investigation of PDR from the perspective of automated planning. Similarly to the planning as satisfiability paradigm, PDR draws its strength from internally employing an efficient SAT-solver. We show that most standard encoding schemes of planning into SAT can be directly used to turn PDR into a planning algorithm. As a non-obvious alternative, we propose to replace the SAT-solver inside PDR by a planningspecific procedure implementing the same interface. This SAT-solver free variant is not only more efficient, but offers additional insights and opportunities for further improvements. An experimental comparison to the state of the art planners finds it highly competitive, solv

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP103%2F10%2F1287" target="_blank" >GAP103/10/1287: PlanEx: Propojení plánování a provádění plánů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2014

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Journal of Artificial Intelligence Research

ISSN

1076-9757

e-ISSN

—

Svazek periodika

2014

Číslo periodika v rámci svazku

50

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

55

Strana od-do

265-319

Kód UT WoS článku

000339311300001

EID výsledku v databázi Scopus

—