将SAT求解与模态演绎结合，显著提升大规模可满足问题求解效率。
Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts
- 用KSP解析器作为预言机生成SAT快捷路径
- 在大规模可满足问题上性能超越单独模块
- 首次实现三者融合且整体优于各部分
本文研究了两种扩展CEGAR-tableaux的SAT快捷方法：一种基于已知的RECAR方法，另一种全新方法利用模态解析证明器KSP作为预言机。通过自研的C++实现CEGARBox++进行实验表明：(1) 使用RECAR的CEGARBox++不具备竞争力；(2) 使用KSP提供SAT快捷路径的CEGARBox++在大尺度可满足问题上显著优于单独的CEGARBox++和KSP。据我们所知，这是首个有效整合SAT、表列法与解析法的模态可满足性求解框架，且整体表现优于其任一部分。
原文摘要 · Abstract (English)
We investigate two approaches for extending CEGAR-tableaux with SAT-shortcuts using a previously known approach called RECAR but also a totally new approach using the modal resolution theorem prover KSP as an oracle. Our experiments using our C++ implementation CEGARBox++ of CEGAR-tableaux show that: (1) CEGARBox++ with RECAR SAT-shortcuts is not competitive (2) CEGARBox++ using KSP to provide SAT-shortcuts is superior to both CEGARBox++ and KSP, particularly on large satisfiable problems. As far as we know, this is the first effective integration of SAT, tableaux and resolution methods for modal satisfiability which performs better than its parts.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。