Factor out the bisection function

Also, create a separate sat() function that just gives one solution.
Clean up the constraint generating function

It's now called generate_constraints() instead of
generate_version_constraints(), the second argument is the max literal rather
than a mapping of literals, and it is no longer on the Resolve class.