Conformant Planning as a Case Study of Incremental QBF Solving

TL;DR

This paper demonstrates that incremental QBF solving, applied to planning under initial state uncertainty, is more efficient than non-incremental methods, with broad potential for other applications.

Contribution

It presents the first empirical study of incremental QBF solving in planning, showing its advantages over non-incremental approaches.

Findings

Incremental QBF solving outperforms non-incremental methods.

Efficient encoding reduces redundancy in QBF instances.

Experimental results validate the approach's effectiveness.

Abstract

We consider planning with uncertainty in the initial state as a case study of incremental quantified Boolean formula (QBF) solving. We report on experiments with a workflow to incrementally encode a planning instance into a sequence of QBFs. To solve this sequence of incrementally constructed QBFs, we use our general-purpose incremental QBF solver DepQBF. Since the generated QBFs have many clauses and variables in common, our approach avoids redundancy both in the encoding phase and in the solving phase. Experimental results show that incremental QBF solving outperforms non-incremental QBF solving. Our results are the first empirical study of incremental QBF solving in the context of planning and motivate its use in other application domains.