TY - JOUR AU - Behnke, Gregor AU - Biundo, Susanne PY - 2018/09/11 Y2 - 2024/03/29 TI - X and more Parallelism. Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more Parallelism: Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more Parallelism JF - Inteligencia Artificial JA - ia VL - 21 IS - 62 SE - Regular Papers DO - 10.4114/intartif.vol21iss62pp75-90 UR - http://journal.iberamia.org/index.php/intartif/article/view/226 SP - 75-90 AB - <p>Linear temporal logic (LTL) provides expressive means to specify temporally extended goals as well as preferences.<br>Recent research has focussed on compilation techniques, i.e., methods to alter the domain ensuring that every solution adheres to the temporally extended goals.<br>This requires either new actions or an construction that is exponential in the size of the formula.<br>A translation into boolean satisfiability (SAT) on the other hand requires neither.<br>So far only one such encoding exists, which is based on the parallel $\exists$-step encoding for classical planning.<br>We show a connection between it and recently developed compilation techniques for LTL, which may be exploited in the future.<br>The major drawback of the encoding is that it is limited to LTL without the X operator.<br>We show how to integrate X and describe two new encodings, which allow for more parallelism than the original encoding.<br>An empirical evaluation shows that the new encodings outperform the current state-of-the-art encoding.</p> ER -