Computer School, National University of Defense Technology, ChangSha, China

---

Abstract—Explaining the causes of infeasibility of Boolean formulas has many practical applications in various fields. A small unsatisfiable subformula provides a succinct explanation of infeasibility and is valuable for applications. In recent years finding unsatisfiable subformulas has been addressed frequently by research works, mostly based on the SAT solvers with DPLL backtrack-search algorithm. However little attention has been concentrated on extraction of unsatisfiable subformulas using incomplete methods. In this paper, we present the definitions of refutation proof and refutation parsing graph, and then propose a resolutionbased local search algorithm to track unsatisfiable subformulas according to the reduced refutation proof of a formula. This approach directly constructs the resolution sequences for proving unsatisfiability with a local search procedure, and then recursively derives unsatisfiable subformulas from the resolve traces. We report and analyze the experimental results on well-known and randomly generated benchmarks.

Index Terms—Boolean satisfiabiltiy, unsatisfiability subformula, refutation proof, local search.

[PDF]

Cite: Jianmin Zhang, Shengyu Shen, and Sikun Li, "Tracking Unsatisfiable Subformulas from Reduced Refutation Proof," Journal of Software vol. 4, no. 1, pp. 42-49, 2009.