Deriving small unsatisfiable cores with dominators

Abstract

The problem of finding a small unsatisfiable core of an unsatisfiable CNF formula is addressed. The proposed algorithm, Trimmer, iterates over each internal node d in the resolution graph that 'consumes' a large number of clauses M (i.e. a large number of original clauses are present in the unsat core only for proving d) and attempts to prove them without the M clauses. If this is possible, it transforms the resolution graph into a new graph that does not have the M clauses at its core. Trimmer can be integrated into a fixpoint framework similarly to Malik and Zhang's fix-point algorithm (RUN_TILL_FIX). We call this option TRIM_TILL_FIX. Experimental evaluation on a large number of industrial CNF unsatisfiable formulas shows that TRIM_TILL_FIX doubles, on average, the number of reduced clauses in comparison to RUN_TILL_FIX. It is also better when used as a component in a bigger system that enforces short timeouts. © Springer-Verlag Berlin Heidelberg 2006.