Factoring out the weight-addition.
Improved documentation.
Some editorial changes.

Introduced also some new auxiliary constructs.
The member "unit" of clause_info doesn't need to be (re-)initialised.
Improved handling of polarities.
Removed clause_info::unit and lit_info::unassigned

As soon as contradictory assignments are found, the assignment process
is stopped now.