---
title: "Planning for Temporally Extended Goals as Propositional Satisfiability"
authors:
  - "Robert Mattmüller"
  - "Jussi Rintanen"
doi: ""
url: "https://ijcai.org/proceedings/2007/317"
pdf: "https://ijcai.org/proceedings/2007/0317.pdf"
venue: "Proceedings of the Twentieth International Joint Conference on Artificial Intelligence"
year: 2007
pages: "1966--1"
track: ""
keywords:
---

# Planning for Temporally Extended Goals as Propositional Satisfiability

Robert Mattmüller, Jussi Rintanen

*Proceedings of the Twentieth International Joint Conference on Artificial Intelligence*, pages 1966--1.

## Abstract

Planning for temporally extended goals (TEGs) expressed as formulae of Linear-time Temporal Logic (LTL) is a proper generalization of classical planning, not only allowing to specify properties of a goal state but of the whole plan execution. Additionally, LTL formulae can be used to represent domain-specific control knowledge to speed up planning. In this paper we extend SAT-based planning for LTL goals (akin to bounded LTL model-checking in verification) to partially ordered plans, thus significantly increasing planning efficiency compared to purely sequential SAT planning. We consider a very relaxed notion of partial ordering and show how planning for LTL goals (without the next-time operator) can be translated into a SAT problem and solved very efficiently. The results extend the practical applicability of SAT-based planning to a wider class of planning problems. In addition, they could be applied to solving problems in bounded LTL model-checking more efficiently.