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.