JOURNAL OF SOFTWARE (JSW)
ISSN : 1796-217X
Volume : 4    Issue : 1    Date : February 2009

Tracking Unsatisfiable Subformulas from Reduced Refutation Proof
Jianmin Zhang, Shengyu Shen, and Sikun Li
Page(s): 42-49
Full Text:
PDF (184 KB)


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 resolution based 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