Sat_solver.S