一致性规划作为增量 QBF 求解的案例研究
计算机科学中的逻辑
2016-04-05 v3 人工智能
摘要
我们将初始状态存在不确定性的规划问题作为增量量化布尔公式 (QBF) 求解的案例进行研究。我们报告了关于将规划实例增量编码为 QBF 序列的工作流的实验结果。为了解决这一增量构建的 QBF 序列，我们使用了通用的增量 QBF 求解器 DepQBF。由于生成的 QBF 具有许多共同的子句和变量，我们的方法在编码阶段和求解阶段都避免了冗余。实验结果表明，增量 QBF 求解优于非增量 QBF 求解。我们的结果是规划背景下增量 QBF 求解的首次实证研究，并推动了其在其他应用领域的使用。
引用
@article{arxiv.1405.7253,
title = {Conformant Planning as a Case Study of Incremental QBF Solving},
author = {Uwe Egly and Martin Kronegger and Florian Lonsing and Andreas Pfandler},
journal= {arXiv preprint arXiv:1405.7253},
year = {2016}
}
备注
added reference to extended journal article; revision (camera-ready, to appear in the proceedings of AISC 2014, volume 8884 of LNAI, Springer)