Improve Linear UNSAT SAT proof performance

[maartenflippo]

With the closing of #216, the performance of unsat-sat degrades. We changed it so that the solver will iteratively increase the lower bound by one each call. However, we can have the following situation:

1. We prove that [x <= 5] -> false
2. Propagation can infer that [x >= 6] /\ ... -> [x >= 20]
3. Now we don't need to prove [x <= 6] -> false, ..., [x <= 18] -> false

[EmirDe]

When doing unsat-sat, I think the way to go is that the algorithm should try to find a solution equal to the lower bound, where lower bound is a variable in the solver. After every call, the solver will by necessity update the lower bound value.

In the example above, each call is with [x <= lb(x)], the first time lb(x) is 5, the second time it is 20 (in the worst case, the lb increases only by one)..