基于 SAT 的完全无关项计算用于网络优化
计算机科学中的逻辑
2011-11-09 v1
摘要
本文描述了一种利用内部无关项进行布尔网络优化的改进方法。改进涉及所计算无关项的类型、范围以及计算方法。我们引入并论证了使用完全无关项 (CDC) 以替代传统使用的相容可观察无关项 (CODC)。为确保针对超大规模工业网络的无关项计算的鲁棒性，实现了一种可选的窗口化方案，该方案能在合理时间内计算 CDC 的重要子集。最后，我们给出了一种基于 SAT 的无关项计算算法，其效率高于基于 BDD 的算法。实验结果证实这些改进在实践中效果良好。与 CODC 相比，完全无关项允许减少文字数量。窗口化保证了鲁棒性，即使对于先前方法无法应用的超大规模基准测试也是如此。SAT 减少了运行时间并增强了鲁棒性，使得无关项计算能够应用于各种其他作用于网络的布尔方法。
引用
@article{arxiv.0710.4695,
title = {SAT-Based Complete Don't-Care Computation for Network Optimization},
author = {Alan Mishchenko and Robert K. Brayton},
journal= {arXiv preprint arXiv:0710.4695},
year = {2011}
}
评论
Submitted on behalf of EDAA (http://www.edaa.com/)