Problem Solving Strategies Using Quantified Boolean Formulas  

Abstract: In recent years we have seen tremendous progress in the area of Boolean satisfiability (SAT) solving and its applications. As a new challenge, the community is     now moving to investigate whether similar advances can be made in the use of Quantified Boolean Formulas (QBF). QBF provides a natural framework for capturing problem solving and planning in multi-agent settings. However, contrarily to single-agent planning, which can be effectively formulated as SAT, we show that a QBF approach to planning in a multi-agent setting leads to significant unexpected computational difficulties. We identify as a key difficulty of the QBF approach the fact that QBF solvers often end up exploring a much larger search space than the natural search space of the original problem. This is in contrast to the experience with SAT approaches. We also show how one can alleviate these problems by introducing two special QBF formulations and a new QBF solution strategy. We present experiments that show the effectiveness of our approach in terms of a significant improvement in performance compared to earlier work in this area. Our work also provides a general methodology for formulating adversarial scenarios in QBF.  Figure 1 shows how to encode problems as Quantified Boolean Formulas and the critical issues that have to be taken into account. Figure 2  shows how to extend  state-of-the-art solvers.

Get here some slides about the project:

:
Figure 1: Encoding Problems as Quantified Boolean Formulas

Figure 2: Extending state-of-the-art QBF solvers