Some refactoring in SAT solver.
Added simulation support.