Application and analysis of unsatisfiable cores on circuits synthesis
2015 Seventh International Conference on Advanced Computational Intelligence (ICACI)(2015)
摘要
Explaining the causes of infeasibility of Boolean formulas has practical applications in various fields. A smallest-cardinality unsatisfiable subset, called a minimum unsatisfiable core, can provide a succinct explanation of infeasibility and is valuable for applications, such as automatic synthesis of decoding circuits. Therefore, two algorithms of deriving minimum unsatisfiable cores, respectively called the greedy-genetic algorithm and branch-and-bound algorithm, are integrated into the synthesis tool. Some standard encoding circuits in communications are adopted as the benchmark. The results show that the greedy-genetic algorithm outperforms the branch-and-bound algorithm on runtime and removed clauses per second. It is also concluded that the unsatisfiable cores play a very important role in automatic synthesis of decoding circuits.
更多查看译文
关键词
unsatisfiable cores,circuit synthesis,Boolean formulas,smallest-cardinality unsatisfiable subset,automatic synthesis,decoding circuits,greedy-genetic algorithm,branch-and-bound algorithm,encoding circuits
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要