BoSy：有界综合的实验框架
计算机科学中的逻辑
2018-03-28 v1
摘要
我们提出 BoSy，一种基于有界综合方法的反应式综合工具。有界综合通过逐步增大其考虑的解的规模界限，来保证所综合实现的最小性。对于每个界限，解的存在性被编码为一个逻辑约束求解问题，并由适当的求解器求解。BoSy 构建了到 SAT、QBF、DQBF、EPR 和 SMT 的有界综合编码，并连接到相应类型的求解器。在求解器支持的情况下，BoSy 将解提取为电路，如有需要，可使用标准硬件模型检查器进行验证。BoSy 赢得了 SYNTCOMP 2016 的 LTL 综合赛道。除了作为综合工具使用外，BoSy 还可用作各类可满足性求解器的实验与性能评估框架。
引用
@article{arxiv.1803.09566,
title = {BoSy: An Experimentation Framework for Bounded Synthesis},
author = {Peter Faymonville and Bernd Finkbeiner and Leander Tentrup},
journal= {arXiv preprint arXiv:1803.09566},
year = {2018}
}
备注
Appeared in the proceedings of CAV 2017