Application and analysis of unsatisfiable cores on circuits synthesis

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.