Polsat：一种组合式 LTL 可满足性求解器
计算机科学中的逻辑
2013-11-08 v1
摘要
本文介绍了一种名为 Polsat 的组合式 LTL 可满足性求解器。为了实现对 LTL 公式的快速可满足性检查，该工具集成了四种具有代表性的 LTL 求解器：pltl、TRP++、NuSMV 和 Aalta。Polsat 的核心思想是并行运行组件求解器以获得最佳整体性能；一旦其中一个求解器终止，便停止所有其他求解器。值得注意的是，Polsat 求解器利用了现代多核计算集群的算力。实证实验表明 Polsat 充分利用了这一优势。此外，Polsat 也是所有 LTL 求解器的测试平台。
引用
@article{arxiv.1311.1602,
title = {Polsat: A Portfolio LTL Satisfiability Solver},
author = {Jianwen Li and Geguang Pu and Lijun Zhang and Yinbo Yao and Moshe Y. Vardi and Jifeng he},
journal= {arXiv preprint arXiv:1311.1602},
year = {2013}
}
备注
11 pages, 1 table, 2 figures