The thesis addresses the problem of
finding a small unsatisfiable core of an unsatisfiable CNF formula. The proposed
algorithm, Core 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 unsatisfiable 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. Core Trimmer can be integrated
into a fixpoint framework. Experimental evaluation on a large number of
industrial CNF unsatisfiable formulas shows that Core Trimmer in the fixpoint
framework doubles, on average ,
the number of reduced clauses in comparison to existing tools. It is also
better when used as a component in a bigger system that enforces short timeouts .
