Implement and and or, also use Light clause instead of real clauses
Extract ite function
Use formula code from minisat+