Reducing Planning to Quantified Boolean Formulae

Question

Why don't we reduce the Planning Problem in AI to the TQBF 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?

Answer 1

If I understand what you're asking:

You want to know why we don't convert a high-level complex problem which has no known solution to a simpler one which we can more easily solve.

Well, consider this: To be able to do so, we'd first need to find an efficient compiler; chances are, it would be harder to run the compiler to convert than it would be to solve the problem.

And, even in a simpler format, there's no fewer computations to solve. Consider this analogy:

I use Conway's Game of Life as a processor. (Please look it up if you don't know what it is) Therefore, I am able to solve in 1 unit of time what a processor takes a long time to simulate (Conway's Game of Life). HOWEVER, if we wanted to have a modern processor SIMULATE A VIRTUAL MACHINE of Conway's Game of Life processor, it would be no faster.

Answer 2

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.