solver3: Remove work rescoring in favor of unit propagation

Instead of expensive rescoring of all outstanding items, use
unit propagation to find new units after conflicts.

We still count the items when adding them; but unless they are
0 or 1, which they should not be, they don't have any effect:
The size field is now effectively static.

If the size of an optional clause changed to 1, it is inserted
a second time, and then moves up to the top of the optional
items per the Work::operator< rules.

0 files changed, 0 insertions, 0 deletions