分布式决策过程的惰性分解
Lazy Decomposition for Distributed Decision Procedures
摘要：
软件和硬件验证自动化工具的日益普及对底层决策过程提出了越来越高的要求。本文提出了一个分布式决策过程（一阶问题）的框架克雷格插值的基础上。公式是以一种懒惰的方式分发的，即，而不使用昂贵的分解算法。潜在的模型被证明是不正确的，通过使用克雷格插值和解。具有挑战性的命题可满足性问题的实验结果表明，我们的方法是能够优于传统的解决技术，即使不使用额外的资源。
英文摘要：
The increasing popularity of automated tools for software and hardware verification puts ever increasing demands on the underlying decision procedures. This paper presents a framework for distributed decision procedures (for first-order problems) based on Craig interpolation. Formulas are distributed in a lazy fashion, i.e., without the use of costly decomposition algorithms. Potential models which are shown to be incorrect are reconciled through the use of Craig interpolants. Experimental results on challenging propositional satisfiability problems indicate that our method is able to outperform traditional solving techniques even without the use of additional resources.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
