starting to separe functions
adding a simple backtracking SAT solver