initial SAT solver implementation and assorted CNF logic changes