Numeric Planning with Disjunctive Global Constraints via SMT. Scala, E., Ramírez, M., Haslum, P., & Thiebaux, S. In Paper abstract bibtex This paper describes a novel encoding for sequential numeric planning into the problem of determining the satisfiability of a logical theory T. We introduce a novel technique, orthogonal to existing work aiming at producing more succinct encodings, that enables the theory solver to "roll up" an unbounded yet finite number of instances of an action into a single plan step, greatly reducing the horizon at which T models valid plans. The technique is then extended to deal with problems featuring "disjunctive global constraints", in which the state space becomes a non-convex n-dimensional polytope. In order to empirically evaluate the encoding, we build a planner, SPRINGROLL, around a state–of–the–art off–the–shelf SMT solver. Experiments on a diverse set of domains are finally reported, and results show the generality and efficiency of the approach.
@inproceedings {icaps16-20,
track = {Main Track},
title = {Numeric Planning with Disjunctive Global Constraints via SMT},
url = {http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13177},
author = {Enrico Scala and Miquel Ramírez and Patrik Haslum and Sylvie Thiebaux},
abstract = {This paper describes a novel encoding for sequential numeric planning into the problem of determining the satisfiability of a logical theory T. We introduce a novel technique, orthogonal to existing work aiming at producing more succinct encodings, that enables the theory solver to "roll up" an unbounded yet finite number of instances of an action into a single plan step, greatly reducing the horizon at which T models valid plans. The technique is then extended to deal with problems featuring "disjunctive global constraints", in which the state space becomes a non-convex n-dimensional polytope. In order to empirically evaluate the encoding, we build a planner, SPRINGROLL, around a state--of--the--art off--the--shelf SMT solver. Experiments on a diverse set of domains are finally reported, and results show the generality and efficiency of the approach.},
keywords = {Classical planning,Planning activities; motions and paths,Planning in mixed discrete / continuous domains}
}
Downloads: 0
{"_id":"p9rw2cNjLeoMFTfrb","bibbaseid":"scala-ramrez-haslum-thiebaux-numericplanningwithdisjunctiveglobalconstraintsviasmt","downloads":0,"creationDate":"2016-03-09T03:04:32.873Z","title":"Numeric Planning with Disjunctive Global Constraints via SMT","author_short":["Scala, E.","Ramírez, M.","Haslum, P.","Thiebaux, S."],"year":null,"bibtype":"inproceedings","biburl":"icaps16.icaps-conference.org/papers.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","track":"Main Track","title":"Numeric Planning with Disjunctive Global Constraints via SMT","url":"http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13177","author":[{"firstnames":["Enrico"],"propositions":[],"lastnames":["Scala"],"suffixes":[]},{"firstnames":["Miquel"],"propositions":[],"lastnames":["Ramírez"],"suffixes":[]},{"firstnames":["Patrik"],"propositions":[],"lastnames":["Haslum"],"suffixes":[]},{"firstnames":["Sylvie"],"propositions":[],"lastnames":["Thiebaux"],"suffixes":[]}],"abstract":"This paper describes a novel encoding for sequential numeric planning into the problem of determining the satisfiability of a logical theory T. We introduce a novel technique, orthogonal to existing work aiming at producing more succinct encodings, that enables the theory solver to \"roll up\" an unbounded yet finite number of instances of an action into a single plan step, greatly reducing the horizon at which T models valid plans. The technique is then extended to deal with problems featuring \"disjunctive global constraints\", in which the state space becomes a non-convex n-dimensional polytope. In order to empirically evaluate the encoding, we build a planner, SPRINGROLL, around a state–of–the–art off–the–shelf SMT solver. Experiments on a diverse set of domains are finally reported, and results show the generality and efficiency of the approach.","keywords":"Classical planning,Planning activities; motions and paths,Planning in mixed discrete / continuous domains","bibtex":"@inproceedings {icaps16-20,\r\n track = {Main Track},\r\n title = {Numeric Planning with Disjunctive Global Constraints via SMT},\r\n url = {http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13177},\r\n author = {Enrico Scala and Miquel Ramírez and Patrik Haslum and Sylvie Thiebaux},\r\n abstract = {This paper describes a novel encoding for sequential numeric planning into the problem of determining the satisfiability of a logical theory T. We introduce a novel technique, orthogonal to existing work aiming at producing more succinct encodings, that enables the theory solver to \"roll up\" an unbounded yet finite number of instances of an action into a single plan step, greatly reducing the horizon at which T models valid plans. The technique is then extended to deal with problems featuring \"disjunctive global constraints\", in which the state space becomes a non-convex n-dimensional polytope. In order to empirically evaluate the encoding, we build a planner, SPRINGROLL, around a state--of--the--art off--the--shelf SMT solver. Experiments on a diverse set of domains are finally reported, and results show the generality and efficiency of the approach.},\r\n keywords = {Classical planning,Planning activities; motions and paths,Planning in mixed discrete / continuous domains}\r\n}\r\n\r\n","author_short":["Scala, E.","Ramírez, M.","Haslum, P.","Thiebaux, S."],"key":"icaps16-20","id":"icaps16-20","bibbaseid":"scala-ramrez-haslum-thiebaux-numericplanningwithdisjunctiveglobalconstraintsviasmt","role":"author","urls":{"Paper":"http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13177"},"keyword":["Classical planning","Planning activities; motions and paths","Planning in mixed discrete / continuous domains"],"metadata":{"authorlinks":{}},"downloads":0,"html":""},"search_terms":["numeric","planning","disjunctive","global","constraints","via","smt","scala","ramírez","haslum","thiebaux"],"keywords":["classical planning","planning activities; motions and paths","planning in mixed discrete / continuous domains"],"authorIDs":[],"dataSources":["iMkx859KiXcegwsin","EZtZjCTnxcdTTyeij"]}