Abstract:Computing unsatisfiable subformulas of Boolean formulas has practical applications in VLSI design and verification. The unsatisfiable subformulas can help electronic design automation tools to rapidly locate the errors and inconsistency. The definitions of resolution refutation and refutation parsing tree, and a heuristic local search algorithm to extract unsatisfiable subformulas from the resolution refutation of a formula are presented. The approach directly constructs the refutation parsing tree for proving unsatisfiability with a local search procedure, and then recursively derives unsatisfiable subformulas. The algorithm combines with reasoning heuristics, dynamic pruning and subsumption elimination method to improve the efficiency. The experimental results show that our algorithm outperforms the similar algorithms on the random benchmarks.