| 引用本文: | 张建民,黎铁军,马柯帆,等.应用不可满足子式的解码电路综合优化方法.[J].国防科技大学学报,2016,38(5):1-6.[点击复制] |
| ZHANG Jianmin,LI Tiejun,MA Kefan,et al.Optimization method of decoding circuits′ synthesis using unsatisfiable subformulas[J].Journal of National University of Defense Technology,2016,38(5):1-6[点击复制] |
|
| |
|
|
| 本文已被：浏览 9514次 下载 6399次 |
| 应用不可满足子式的解码电路综合优化方法 |
| 张建民, 黎铁军, 马柯帆, 肖立权 |
|
(国防科技大学 计算机学院， 湖南 长沙 410073)
|
| 摘要: |
| 解释布尔公式不可满足的原因在很多领域都具有实际的应用需求，而最小不可满足子式能够为诸如电路的自动综合等应用领域中的不可满足原因提供最精确的解释。因此，将两种能够高效求解最小不可满足子式的算法——分支-限界算法与贪心遗传算法，集成到解码电路的自动综合工具中。采用通信领域的标准编码电路作为测试集，将两种算法进行对比。实验结果表明，在运行时间与每秒剔除的短句数方面，贪心遗传算法优于分支-限界算法；不可满足子式在解码电路的自动综合过程中发挥重要作用。 |
| 关键词: 电路综合 形式化方法 可满足性求解 不可满足子式 |
| DOI：10.11887/j.cn.201605001 |
| 投稿日期：2015-11-17 |
| 基金项目:国家自然科学基金资助项目（61103083，61133007）；国家重点研发计划资助项目（2016YFB0200203） |
|
| Optimization method of decoding circuits′ synthesis using unsatisfiable subformulas |
| ZHANG Jianmin, LI Tiejun, MA Kefan, XIAO Liquan |
|
(College of Computer, National University of Defense Technology, Changsha 410073, China)
|
| Abstract: |
| 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. |
| Keywords: circuit synthesis formal method satisfiability solving unsatisfiable subformula |
|
|
