SatELite

Note! Since the introduction of MiniSat 2, SatELite as a tool is obsolete.

SatELite is a CNF minimizer, intended to be used as a preprocessor to the SAT solver. It is designed to compress the CNF fast enough not to be a bottle neck, and is particularly aimed at improving SAT encodings resulting from translation of netlists (combinational boolean circuits).

With MiniSat as backend — the "GTI" component — SatELiteGTI won all three industrial categories in the SAT 2005 competition. The stand-alone MiniSat took all the second places in the same categories.

Running SatELite...
	SatELite_v1.0_linux	-	Statically linked Linux binary.
	SatELite_v1.0_macOS	-	Mac OS binary (thanks to Carsten Sinz).
	SatELite_manual.txt	-	A few notes on how to use SatELite.
	sat2005_submission.zip	-	Source code for SatELite and MiniSat (the version submitted for the SAT 2005 contest, not very tidy)
Understanding SatELite...
	SatELite.pdf	-	"Effective Preprocessing in SAT through Variable and Clause Elimination", Niklas Een and Armin Biere, published in the SAT 2005 proceedings. The paper describes and evaluates the SatELite preprocessing techniques.
	SatELite paper data	-	Here you can find all the benchmark and individual bencmark results presented in the paper, as well as the exact binaries used (if you want to reproduce the experiments on your system).
	SatELite_demo.zip	-	A Linux and a Cygwin binary, giving a visual demo of SatELite running (positivly cool! try it!)
	SatELite_slides.sxi	-	Slides for the talk given at SAT 2005 in OpenOffice format.
	SatELite_slides.pdf	-	Ditto in PDF format.