Refactor start()

Refactor the start() function that initializes the search.
This function now assigns all units and assumptions unconditionally.

The user is responsible to call start() before running search()
and after each call to reset().

This should clean up solver code that explicitly deals with
units, assumptions and decision levels.