为什么我们不将 人工智能中的规划问题 规约到 SAT 的 TQBF 版本，并在实际求解器中使用它呢？

实际上，许多规划问题都被“编译”或规约到 SAT 问题，然后由 SAT 求解器解决。问题在于，由于规划是 PSPACE 完全问题，而 SAT 是 NP 完全问题，因此可能需要指数数量的文字。

那么，为什么实际的规划器会使用这种方法呢？ 为什么我们不都解决 TQBF SAT，然后将规划“编译”到 TQBF，反正这应该只需要多项式时间？

回答：

这已经有人做过了。

通常，TQBF 用于建模符合性规划，但确实存在将纯命题逻辑规划问题编码为（多项式大小的）TQBF 公式的方法。

主要的缺点是，尽管我们得到了一个更小的公式，但它并不一定更容易解决。 TQBF 求解的研究成熟度远不如 SAT 求解，并且将规划表示为 TQBF 在性能方面仍然落后。

这是一篇详细介绍此类转换的出版物（我的）：

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