Explaining the causes of infeasibility of Boolean formulae has practical applications in various fields.A smallest-cardinality unsatisfiable subformula can provide a succinct explanation of infeasibility,and help automatic tools to rapidly locate the errors,and determine the underlying reasons for the failure.We present the relationship between maximal satisfiability and minimum unsatisfiability.Based on the relationship,a compounded greedy genetic algorithm and an ant colony algorithm are proposed to derive a minimum unsatisfiable subformula.We report experimental results on practical benchmarks,as compared with the best known branch-and-bound algorithm.The results show that two algorithms strongly outperform the branch-and-bound algorithm,and the compounded greedy genetic algorithm outperforms the ant colony algorithm on both efficiency and size of unsatisfiable subformulae.