===============================================================================
The preprocessor and SAT solver SatELite
===============================================================================
You can get some help by running "SatELite -h", but it is pretty cryptic:
SatELite [OUTPUTS: [ []]]
options: {+,-}{cs1,csk,ve,s0,s1,s2,r,(de,ud,h1)=ve+,pl,as,all,det, pre,ext,mod}
and: --{help,defaults,verbosity=}
In general: '+' turns an option on, '-' turns it off. Type "SatELite
--defaults" to see the default values. An empty '-' turns everything off (try
"SatELite - --defaults").
The most important options are:
+pre -- Only use the preprocessor. Otherwise SatELite will invoke its
built in SAT solver (which is not very good). ALTERNATIVELY:
Specify an output file (second argument); this enables '+pre'
implicitly.
+ve+ -- Turn on the more expensive simplifications: "de" definitional
elimination, "ud" unit definitions, and "h1" hyper-unary
resolution.
If you tie SatELite together with another SAT solver, you can use the extra
output files for "variable map" and "eliminated clauses". Look at the
'SatELiteGTI' script for details on this.
// Niklas