Core Trimmer

This is the homepage of CoreTrimmer, a tool for extracting small unsatisfiable cores from unsatisfiable SAT formulas in CNF. 


CoreTrimmer, iterates over each internal node d in the resolution graph that dominates (`consumes') a large number of clauses M(d) (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(d) clauses. If this is possible, it transforms the resolution graph into a new graph that does not have these clauses at its core. When combined in a fix-point framework the algorithm is called trim-till-fix.

Core Trimmer




Contact Information

Ofer Strichman

Maya Koifman

Roman Gershman