Lazy Compilation in Classical Planning (Extended Abstract)

Authors

  • Zuzana Fílová Czech Technical University in Prague, Faculty of Information Technology
  • Pavel Surynek Czech Technical University in Prague, Faculty of Information Technology

Keywords:

Search In Boolean Satisfiability, Problem Compilation, Problem Solving Using Search

Abstract

Classical planning is a task of finding a sequence of actions that achieve a given goal. One of many approaches to classical planning is compilation into propositional satisfiability (SAT). In this work, we propose a new method that uses lazy compilation into SAT. Different from the standard compilation method, lazy compilation constructs the target propositional formula step by step while the SAT solver is consulted at each step and refinements of the formula are suggested according to SAT solver's answers. The performed experiments pointed out that lazy compilation has the potential to improve the performance of the planners.

Downloads

Published

2022-07-17