make binary clauses in Sat implicit, and remove simplify (to be redone later)