Sciweavers

CAV
2006
Springer

Deriving Small Unsatisfiable Cores with Dominators

14 years 4 months ago
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.
Roman Gershman, Maya Koifman, Ofer Strichman
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CAV
Authors Roman Gershman, Maya Koifman, Ofer Strichman
Comments (0)