A proof engine approach to solving combinational design automation problems
A proof engine approach to solving combinational design automation problems
复制标题
解决组合设计自动化问题的证明引擎方法
DOI：
10.1145/513918.514101
复制
发表时间：
2002
期刊：
影响因子：
--
通讯作者：
Z. Hanna
中科院分区：
文献类型：
--
作者：
G. Andersson;Per Bjesse;B. Cook;Z. Hanna
有许多方法可用于解决编码为重言式或可满足性检查的组合设计自动化问题。不幸的是，不存在一个单一的分析，使足够的性能为所有感兴趣的问题，因此，它是至关重要的是能够联合收割机的方法。在本文中，我们提出了一个证明引擎框架，其中个别分析被视为不同的证明状态之间的策略功能。通过定义我们的证明引擎，我们可以组合策略来形成新的，更强大的策略，我们实现了各个方法之间的协同效应。由此产生的框架使我们能够开发一小部分强大的复合默认策略。我们描述了几种策略和它们的相互作用;其中一种策略，变量实例化，是新的。实验结果表明，我们的默认策略可以实现高达几个数量级的速度相比，基于BDD的技术和基于搜索的可满足性求解器，如ZCHAFF我们的方法的强度。
There are many approaches available for solving combinational design automation problems encoded as tautology or satisfiability checks. Unfortunately there exists no single analysis that gives adequate performance for all problems of interest, and it is therefore critical to be able to combine approaches. In this paper, we present a proof engine framework where individual analyses are viewed as strategies-functions between different proof states. By defining our proof engine in such a way that we can compose strategies to form new, more powerful, strategies we achieve synergistic effects between the individual methods. The resulting framework has enabled us to develop a small set of powerful composite default strategies. We describe several strategies and their interplay; one of the strategies, variable instantiation, is new. The strength of our approach is demonstrated with experimental results showing that our default strategies can achieve up to several magnitudes of speed-up compared to BDD-based techniques and search-based satisfiability solvers such as ZCHAFF.