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

The algorithm Core Trimmer was presented at CAV 2006 and the article can be downloaded here.
The source files can be downloaded here (zip) or here (tgz).
Maya's thesis containing more extensive information regarding theoretical background, the algorithm and experimental results can be downloaded here.

Contact Information

Dr. Ofer Strichman ofers@ie.technion.ac.il

Maya Koifman koifmanm@tx.technion.ac.il

Roman Gershman gershman@cs.technion.ac.il

Dr. Ofer Strichman	ofers@ie.technion.ac.il
Maya Koifman	koifmanm@tx.technion.ac.il
Roman Gershman	gershman@cs.technion.ac.il

Core Trimmer

Summary

Downloads

Contact Information

Links