中文摘要：

解释布尔公式不可满足的原因在诸如形式化验证与电子设计自动化等众多领域中都具有非常重要的理论与应用价值．不可满足子式能够为布尔公式不可满足的原因提供精确的解释，帮助应用领域的自动化工具迅速定位错误，诊断问题失败的本质缘由．针对近年来出现的许多求解布尔不可满足子式的研究工作，根据算法的类型归类比较，对各种求解方法进行了概述评论，并简要介绍了在该领域所做的一些研究工作．最后讨论了布尔不可满足子式的求解方法目前面临的主要挑战，并对今后的研究方向进行了展望．

英文摘要：

Explaining the causes of infeasibility of Boolean formulae has theoretical importance and practical applications in various fields, such as formal verification and electronic design automation. An unsatisfiable subformula can provide a succinct explanation of infeasibility, and help application automatic tools to rapidly locate the errors, and to determine the underlying reasons for the failure. In recent years, there are many different contributions to research on extraction of Boolean unsatisfiable subformulae, due to the increasing importance in numerous practical applications. The existing algorithms are introduced and compared according to their types. Then we present our recent research works to derive unsatisfiable subformulae. Finally, we discuss the current challenges of methods to extract Boolean unsatisfiable subformulae, and outline the future research directions.