Relaxed Exists-Step Plans in Planning as SMT

Relaxed Exists-Step Plans in Planning as SMT. Bofill, M., Espasa, J., & Villaret, M. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, pages 563–570, Melbourne, Australia, August, 2017. International Joint Conferences on Artificial Intelligence Organization.

Paper doi abstract bibtex

Planning Modulo Theories (PMT), inspired by Satisﬁability Modulo Theories (SMT), allows the integration of arbitrary ﬁrst order theories, such as linear arithmetic, with propositional planning. Under this setting, planning as SAT is generalized to planning as SMT. In this paper we introduce a new encoding for planning as SMT, which adheres to the relaxed relaxed ∃-step (R2∃-step) semantics for parallel plans. We show the beneﬁts of relaxing the requirements on the set of actions eligible to be executed at the same time, even though many redundant actions can be introduced. We also show how, by a MaxSMT based post-processing step, redundant actions can be efﬁciently removed, and provide experimental results showing the beneﬁts of this approach.

@inproceedings{bofill_relaxed_2017,
	address = {Melbourne, Australia},
	title = {Relaxed {Exists}-{Step} {Plans} in {Planning} as {SMT}},
	isbn = {978-0-9992411-0-3},
	url = {https://www.ijcai.org/proceedings/2017/79},
	doi = {10.24963/ijcai.2017/79},
	abstract = {Planning Modulo Theories (PMT), inspired by Satisﬁability Modulo Theories (SMT), allows the integration of arbitrary ﬁrst order theories, such as linear arithmetic, with propositional planning. Under this setting, planning as SAT is generalized to planning as SMT. In this paper we introduce a new encoding for planning as SMT, which adheres to the relaxed relaxed ∃-step (R2∃-step) semantics for parallel plans. We show the beneﬁts of relaxing the requirements on the set of actions eligible to be executed at the same time, even though many redundant actions can be introduced. We also show how, by a MaxSMT based post-processing step, redundant actions can be efﬁciently removed, and provide experimental results showing the beneﬁts of this approach.},
	language = {en},
	urldate = {2023-05-15},
	booktitle = {Proceedings of the {Twenty}-{Sixth} {International} {Joint} {Conference} on {Artificial} {Intelligence}},
	publisher = {International Joint Conferences on Artificial Intelligence Organization},
	author = {Bofill, Miquel and Espasa, Joan and Villaret, Mateu},
	month = aug,
	year = {2017},
	pages = {563--570},
}

Downloads: 0

{"_id":"5vFvhwh7znQKvNfnR","bibbaseid":"bofill-espasa-villaret-relaxedexistsstepplansinplanningassmt-2017","author_short":["Bofill, M.","Espasa, J.","Villaret, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Melbourne, Australia","title":"Relaxed Exists-Step Plans in Planning as SMT","isbn":"978-0-9992411-0-3","url":"https://www.ijcai.org/proceedings/2017/79","doi":"10.24963/ijcai.2017/79","abstract":"Planning Modulo Theories (PMT), inspired by Satisﬁability Modulo Theories (SMT), allows the integration of arbitrary ﬁrst order theories, such as linear arithmetic, with propositional planning. Under this setting, planning as SAT is generalized to planning as SMT. In this paper we introduce a new encoding for planning as SMT, which adheres to the relaxed relaxed ∃-step (R2∃-step) semantics for parallel plans. We show the beneﬁts of relaxing the requirements on the set of actions eligible to be executed at the same time, even though many redundant actions can be introduced. We also show how, by a MaxSMT based post-processing step, redundant actions can be efﬁciently removed, and provide experimental results showing the beneﬁts of this approach.","language":"en","urldate":"2023-05-15","booktitle":"Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence","publisher":"International Joint Conferences on Artificial Intelligence Organization","author":[{"propositions":[],"lastnames":["Bofill"],"firstnames":["Miquel"],"suffixes":[]},{"propositions":[],"lastnames":["Espasa"],"firstnames":["Joan"],"suffixes":[]},{"propositions":[],"lastnames":["Villaret"],"firstnames":["Mateu"],"suffixes":[]}],"month":"August","year":"2017","pages":"563–570","bibtex":"@inproceedings{bofill_relaxed_2017,\n\taddress = {Melbourne, Australia},\n\ttitle = {Relaxed {Exists}-{Step} {Plans} in {Planning} as {SMT}},\n\tisbn = {978-0-9992411-0-3},\n\turl = {https://www.ijcai.org/proceedings/2017/79},\n\tdoi = {10.24963/ijcai.2017/79},\n\tabstract = {Planning Modulo Theories (PMT), inspired by Satisﬁability Modulo Theories (SMT), allows the integration of arbitrary ﬁrst order theories, such as linear arithmetic, with propositional planning. Under this setting, planning as SAT is generalized to planning as SMT. In this paper we introduce a new encoding for planning as SMT, which adheres to the relaxed relaxed ∃-step (R2∃-step) semantics for parallel plans. We show the beneﬁts of relaxing the requirements on the set of actions eligible to be executed at the same time, even though many redundant actions can be introduced. We also show how, by a MaxSMT based post-processing step, redundant actions can be efﬁciently removed, and provide experimental results showing the beneﬁts of this approach.},\n\tlanguage = {en},\n\turldate = {2023-05-15},\n\tbooktitle = {Proceedings of the {Twenty}-{Sixth} {International} {Joint} {Conference} on {Artificial} {Intelligence}},\n\tpublisher = {International Joint Conferences on Artificial Intelligence Organization},\n\tauthor = {Bofill, Miquel and Espasa, Joan and Villaret, Mateu},\n\tmonth = aug,\n\tyear = {2017},\n\tpages = {563--570},\n}\n\n\n\n\n\n\n\n","author_short":["Bofill, M.","Espasa, J.","Villaret, M."],"key":"bofill_relaxed_2017","id":"bofill_relaxed_2017","bibbaseid":"bofill-espasa-villaret-relaxedexistsstepplansinplanningassmt-2017","role":"author","urls":{"Paper":"https://www.ijcai.org/proceedings/2017/79"},"metadata":{"authorlinks":{}},"downloads":0,"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/matteocarde","dataSources":["BLJPWpPi3hneTGaPF"],"keywords":[],"search_terms":["relaxed","exists","step","plans","planning","smt","bofill","espasa","villaret"],"title":"Relaxed Exists-Step Plans in Planning as SMT","year":2017}