make Sat.cleanup only do stuff when necessary
make occurrence lists lazy and precise
put static assignment in separate module and redo the framework for variable elimination