通过仪器化 SMT 求解器求解混合网络可达性问题
人工智能
2016-09-14 v1
摘要
PDDL+ 规划的语义根植于混合自动机（HA），近期工作表明它可以被建模为 HA 网络。将非线性 PDDL+ 规划作为 HA 处理时，其复杂性要求在空间和时间上均高效的推理。遗憾的是，现有的求解器要么不处理非线性动力学，要么不原生支持自动机网络。我们提出了一种名为 HNSolve 的新算法，它在将非线性 PDDL+ 规划作为 HA 的网络编码进行推理时，指导 dReal Satisfiability Modulo Theories（SMT）求解器的变量选择。HNSolve 通过求解 HA 网络的离散抽象与 dReal 紧密集成。HNSolve 在 HA 网络上寻找忽略连续变量但遵守模式跳转和同步标签的复合运行。HNSolve 可容许地检测离散抽象中的死端，并发布冲突子句以修剪 SMT 求解器的搜索。我们在 PDDL+ 基准问题上评估了 HNSolve 算法的优势，并展示了其相对于先前工作的性能。
引用
@article{arxiv.1609.03847,
title = {Instrumenting an SMT Solver to Solve Hybrid Network Reachability Problems},
author = {Daniel Bryce and Sergiy Bogomolov and Alexander Heinz and Christian Schilling},
journal= {arXiv preprint arXiv:1609.03847},
year = {2016}
}