Relaxing non-interference requirements in parallel plans

Miquel Bofill, Joan Espasa, Mateu Villaret

Research output: Contribution to journalArticlepeer-review


The aim of being able to reason about quantities, time or space has been the main objective of the many efforts on the integration of propositional planning with extensions to handle different theories. Planning modulo theories (PMTs) are an approximation inspired by satisfiability modulo theories (SMTs) that generalize the integration of arbitrary theories with propositional planning. Parallel plans are crucial to reduce plan lengths and hence the time needed to reach a feasible plan in many approaches. Parallelization of actions relies on the notion of (non-)interference, which is usually determined syntactically at compile time. In this paper we define a semantic notion of interference between actions in PMT. Apart from being strictly stronger than any syntactic notion of interference, we show how semantic interference can be easily and efficiently checked by calling an off-the-shelf SMT solver at compile time, constituting a technique orthogonal to the solving method.
Original languageEnglish
Pages (from-to)45–71
Number of pages27
JournalLogic Journal of the IGPL
Issue number1
Early online date1 Aug 2019
Publication statusE-pub ahead of print - 1 Aug 2019


  • Planning
  • Planning modulo theories
  • SMT
  • Planning as satisfiability
  • Parallel plans


Dive into the research topics of 'Relaxing non-interference requirements in parallel plans'. Together they form a unique fingerprint.

Cite this