Some small simplifications.
Detecting satisfiability earlier, and saving a bit of work at the root.
Introduced macro PURE_LITERALS.

By default now again no elimination of pure literals.
Improved explanations of weights.