Core Trimmer

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

Summary

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

 

Downloads

 

Contact Information

Ofer Strichman

ofers@ie.technion.ac.il

Maya Koifman

koifmanm@tx.technion.ac.il

Roman Gershman

gershman@cs.technion.ac.il

Links