将规划简化为量化布尔公式
为什么我们不将人工智能中的规划问题减少到 实际求解器中的 SAT 的 TQBF 版本。
许多规划问题实际上都是“编译”或简化为 SAT 问题，然后由 SAT 求解器解决。问题是，由于规划是 PSPACE Complete 的，而 SAT 是 NP Complete 的，因此可能需要指数数量的文字。
那么，为什么实际的规划者会使用这种方法呢？为什么我们不都解决 TQBF SAT，然后将规划“编译”为 TQBF，无论如何，这应该只需要多项式时间？
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?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
这已经完成了。
通常，TQBF 用于对一致性规划进行建模，但确实存在将纯命题逻辑规划问题编码为（多项式大小）TQBF 公式的情况。
主要缺点是，虽然我们有一个小得多的公式，但它不一定更容易解决。 TQBF 求解远没有解决 SAT 的研究那么成熟，而作为 TQBF 的规划在性能上仍然落后一些。
这是一份详细介绍这种转变的出版物（我的）：
http： //users.cecs.anu.edu.au/~ssanner/ICAPS_2010_DC/Abstracts/cashmore.pdf
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 求解器经过高度优化，能够利用问题内部的结构。他们在大多数问题上都很快（但他们不可能在所有问题上都很快，因为 SAT 很难）。
因此，通过将您的规划问题编译成 SAT 实例，您就能够利用现代 SAT 求解器开发中的所有工作。您可能会丢失一些与规划问题相关的结构，您可以通过直接编写规划器来利用这些结构。
也许，当巧妙地编译规划问题并利用此步骤中的规划结构时，您将能够获得更简单的 SAT 实例。但这样做时，人们可能会说你正在尝试再次解决规划问题，只是通过另一种计算模型（SAT 求解器而不是随机存取存储器机器或更间接的 LISP，等等）。
那么为什么不TQBF呢？
显然，因为还没人尝试过（我无法确认）。也许以前没有人有这个想法，或者可能没有人认为当前的 TQBF 求解器足够聪明，可以快速解决编译后的规划问题 - 至少比最先进的规划器更快。
我对 TQBF 求解器场景了解不多。事实上，我以前从未听说过像通用 TQBF 求解器这样的东西（一般不包括逻辑编程）。我认为这比 SAT 难多了（尚未证实，假设 Deolalikar 是错的）。
所以，继续尝试吧。如果成功，您可以在此处发布您出版物的链接。
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.