Research Advances in Methods of Extracting Boolean Unsatisfiable Subformulae

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.