{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,7]],"date-time":"2024-08-07T07:40:07Z","timestamp":1723016407807},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9]]},"abstract":"Property Directed Reachability (PDR) is a relatively new SAT-based search paradigm for classical AI planning. Compared to earlier SAT-based paradigms, PDR proceeds without unrolling the system transition function, and therefore without having the underlying procedure reason about potentially computationally expensive multi-step formulae. By maintaining a queue of obligations - i.e., a state at a timestep - and knowledge about what is possible at each planning step, PDR iteratively evaluates whether an obligation can be progressed by one step towards the goal. We develop and evaluate two new distributed PDR algorithms for planning, and additionally implement serial and portfolio PDR algorithms for planning. We are the first to consider distributed PDR for planning and the first to consider PDR based on incremental SAT solving in that setting. Our first new algorithm, PS-PDR, evaluates many obligations independently in parallel using a pool of incremental SAT workers. PS-PDR is unique amongst distributed PDR algorithms in centrally maintaining a single queue of obligations, enabling an efficient focused search compared to a PDR portfolio. Our second new algorithm, PD-PDR, sequences subproblems according to the compositional structure of the concrete problem at hand. Subproblems are solved independently in parallel, with a concrete plan obtained by combining subproblem plans. Our experimental evaluation exhibits strong runtime gains for both new algorithms in both satisfiable and unsatisfiable planning benchmarks.<\/jats:p>","DOI":"10.24963\/kr.2023\/16","type":"proceedings-article","created":{"date-parts":[[2023,7,31]],"date-time":"2023-07-31T22:27:47Z","timestamp":1690842467000},"page":"156-166","source":"Crossref","is-referenced-by-count":0,"title":["Property Directed Reachability for Planning Revisited"],"prefix":"10.24963","author":[{"given":"Ava","family":"Clifton","sequence":"first","affiliation":[{"name":"Australian National University"}]},{"given":"Charles","family":"Gretton","sequence":"additional","affiliation":[{"name":"Australian National University"}]}],"member":"10584","event":{"number":"20","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","Academic College of Tel-Aviv","European Association for Artificial Intelligence","National Science Foundation"],"acronym":"KR-2023","name":"20th International Conference on Principles of Knowledge Representation and Reasoning {KR-2023}","start":{"date-parts":[[2023,9,2]]},"theme":"Artificial Intelligence","location":"Rhodes, Greece","end":{"date-parts":[[2023,9,8]]}},"container-title":["Proceedings of the Twentieth International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2023,7,31]],"date-time":"2023-07-31T22:28:04Z","timestamp":1690842484000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2023\/16"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2023,9]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2023\/16","relation":{},"subject":[],"published":{"date-parts":[[2023,9]]}}}