Reducing Planning to Quantified Boolean Formulae

Why don't we reduce the Planning Problem in AI to the T开发者_StackOverflow社区QBF Version of SAT in practical solvers.

Many planning problems are in practice "compiled down" or reduced to the SAT problem, which is in turn solved by SAT Solvers. The problem is that , since planning is PSPACE Complete, and SAT is NP Complete, an exponential number of literals may be required.

Why, then, do practical planners use this approach? Why don't we all solve TQBF SAT and then "compile" Planning down to TQBF, which should only take Polynomial time anyway?

This has already been done.

Generally TQBF is used to model conformant planning, but there do exist encodings of purely propositional logic planning problems to (polynomially-sized) TQBF formulae.

The main drawback is that, although we have a much smaller formula, it's not neccessarily easier to solve. TQBF solving is no way near as mature as the research into solving SAT, and Planning as TQBF is still some way behind in performance.

Here is one publication detailing such a transformation (mine):

http://users.cecs.anu.edu.au/~ssanner/ICAPS_2010_DC/Abstracts/cashmore.pdf

SAT solvers today are highly optimized and able to exploit structure inside the problems. They are very fast on most problems (but they can't be fast on all, because SAT is hard).

So by compiling down your planning problem into an instance of SAT, you are able to exploit all the work that went into the development of modern SAT solvers. You'll probably loose some structure related to the planning problem, which you could have exploited by writing a planner directly.

Maybe, when cleverly compiling down the planning problem and exploiting the planning structure in this step you'll be able to obtain easier SAT instances. But when doing so, one could say you're trying to solve the planning problem again, just by the means of another computation model (SAT-solver instead of random access memory machine or more indirectly LISP, whatever).

So why not TQBF?

Obviously, because no one has tried, yet (which I can't confirm). Maybe no one had this idea before or maybe no one thought that current TQBF-solvers are smart enough to quickly solve the compiled down planning problems - at least more quickly than the state-of-the-art planners.

I'm not well informed in the TQBF-solver scene. Actually, I've never heard of something like a general TQBF-solver before (excluding logic programming in general). I think it's way harder to do than SAT (which hasn't been proven yet, supposed Deolalikar is wrong).

So, go ahead and try it. You can post a link to your publication here if you succeed.