Efficient planning with QBF-solvers

Abstract

Für alltägliche Probleme haben wir gute Lösungsmethoden entwickelt. Wird das Problem komplexer, so erkennen wir, wie schwer dessen Planung ist. Automatisches Planen mithilfe von Computerunterstützung soll genau da ansetzen, wo durchschnittliche Personen keine guten Lösungen mehr finden. Planen ist eine der klassischen Gebiete der Künstlichen Intelligenz. Prominente Anwendungsgebiete reichen vom "Remote Agent" in der "Deep Space One" Mission bis hin zu Entscheidungsunterstützungssytemen für Katastrofenhilfe. Planen ist die Aufgabe, eine Sequenz von Aktionen zu finden, die zu einem Zustand führen, in dem das Ziel erfüllt ist.<br />Klassisches Planen mit vollständiger Information, deterministischen Aktionen, Pläne mit polynomieller Länge, etc. ist schon NP-vollständig.<br />Diese Form wurde in den letzten Jahrzehnten sehr intensiv erforscht. In der Realität haben wir jedoch nur unvollständige Information, was die Komplexität auf die zweite Stufe der polynomiellen Hierarchie anhebt. In letzter Zeit wird auch diesem Gebiet in der Forschung mehr Aufmerksamkeit gewidmet. In dieser Arbeit zeigen wir, wie eine Planungssprache für klassisches Planen geschickt erweitert werden kann, um unvollständige Information auszudrücken. Zusätzlich werden wir eine schwache Form von Ungleichheit einführen und beweisen, dass Planen in dieser Sprache Sigma2P-vollständig ist. Weiters werden wir ein Planungstool entwickeln, welches das Planungsproblem auf das Erfüllbarkeitsproblem von quantifizierten, aussagenlogischen Formeln reduziert. Die Pläne von diesem Tool ist optimal bezüglich der Planlänge. Dieses Planungstool kann sowohl Planungsprobleme mit vollständiger als auch mit unvollständiger Information lösen. Wir werden einige Herausforderungen aufzeigen, um diesen exakten Ansatz wettbewerbsfähig zu machen. Hierfür werden wir eine Reihe von Optimierungen vorstellen, die diese Herausforderungen unter Kontrolle bringen. Zusätzlich werden wir einen Benchmark entwickeln, um unser Tool zu testen.

Planning is everywhere. In our everyday life we have developed very fast methods to produce good plans for simple tasks. However, when the complexity of the problem grows, we realize how difficult planning can be. Automated planning with the help of computers should start where average people are lost in generating plans. Planning has a long history in artificial intelligence (AI) and plays a crucial role in this field.<br />Prominent areas of application are for example the Remote Agent in NASA's "Deep Space One" mission and emergency decision support systems.<br />Given an initial state and a set of actions with preconditions and effects, the task of planning is to find a sequence of actions that lead to a state in which the goal is achieved. The classical planning problem with complete information, deterministic actions, plans of polynomial length, etc. already is NP-complete. This form of planning has been studied very intensively during the last decades. However, in real world, we only have incomplete information. This raises the complexity of the planning problem to the second level of the polynomial hierarchy (Σ2 P-complete). Recently, this form of planning got more attention in research.<br />In this thesis, we show how to extend a state-of-the-art planning language for classical planning to model incomplete information. In addition, we introduce a weak form of inequality and then prove that these extensions exactly cover planning with incomplete information i.<br />e. planning in the grounded language is Σ2P-complete. We implement a solver that reduces the planning problem in our language to the satisfiability problem of quantified Boolean formulas. The solutions from our solver are optimal in terms of the plan length and the planner is able to solve tasks with complete and incomplete information. We also discuss the challenges in implementing an exact solver following this approach and present several optimizations. Furthermore, we develop a new benchmark scenario and create a generator for it.