摘要
解释布尔公式不可满足的原因在很多领域都具有实际的应用需求,而最小不可满足子式能够为诸如电路的自动综合等应用领域中的不可满足原因提供最精确的解释。因此,将两种能够高效求解最小不可满足子式的算法——分支-限界算法与贪心遗传算法,集成到解码电路的自动综合工具中。采用通信领域的标准编码电路作为测试集,将两种算法进行对比。实验结果表明,在运行时间与每秒剔除的短句数方面,贪心遗传算法优于分支-限界算法;不可满足子式在解码电路的自动综合过程中发挥重要作用。
Explaining the causes of unsatisfiability of the Boolean formulas has many real applications in various fields. The minimum unsatisfiable subformulas can provide most accurate explanations for the causes of infeasibility in many application fields such as the automatic circuits' synthesis. Therefore, two best algorithms of extracting the minimum unsatisfiable subformulas, respectively called the branch - and - bound algorithm and greedy genetic algorithm, were integrated into the automatic synthesis tool of decoding circuits. Adopting the standard encoding circuits in communication fields as the benchmarks, the study compared and analyzed the two algorithms. The experimental results show that the greedy genetic algorithm outperforms the branch - and - bound algorithm on runtime and removed clauses per second. The results also show that the unsatisfiable subformulas play an important role in the process of synthesizing automatically the decoding circuits.
作者
张建民
黎铁军
马柯帆
肖立权
ZHANG Jianmin;LI Tiejun;MA Kefan;XIAO Liquan(College of Computer, National University of Defense Technology, Changsha 410073 , China)
出处
《国防科技大学学报》
EI
CAS
CSCD
北大核心
2016年第5期1-6,共6页
Journal of National University of Defense Technology
基金
国家自然科学基金资助项目(61103083
61133007)
国家重点研发计划资助项目(2016YFB0200203)
关键词
电路综合
形式化方法
可满足性求解
不可满足子式
circuit synthesis
formal method
satisfiability solving
unsatisfiable subformula