boolean SAT solver recursion

Question

I need to make a SAT-solver for a homework assignment. my input gives me n variables x1,x2...xn, and M clauses which are disjuntions of literals , represented by a list of lists ex. [[-1,2,3],[2,-3],[1,-3]] where [-1,3],[2,-3] means (~X1 or X3) and (X2 or ~X3).

My plan is to implement a backtracking solution, where I first choose X1 = False, then recursively check the equation for each other variable.

My problems is how to set up the recursion. I have 2 functions, one which checks for contradictions in my program, and one which simplifies the expression based on the truth value selected for a variable.

def contradiction(clauses):
  for clause in clauses:
    if clause == ['F']: #checks if any clause evaluates to False
      return True
    for other in clauses:
      if len(clause)==1 and len(other)==1:
        if clause[0] == -other[0]:  #checks if clauses Xi and ~Xi exist
          return True
  return False

def simplification(clauses, value):
  new_clauses = [i for i in clauses]
  for i in range(len(new_clauses)):
    if -(value) in new_clauses[i]: #for assignment Xi, removes ~Xi from each clause, + vice versa
      del new_clauses[i][new_clauses[i].index(-value)]
      if new_clauses[i] == []:
        new_clauses[i] = ['F']
    if value in new_clauses[i]: #for value Xi, removes clauses satisfied by Xi
      new_clauses [i] = []
  return new_clauses  

I wish to start at X1 and go through recursively down to Xn, stopping the process if a contradiction is found. A non recursive solution is fine as well.

EDIT: this is what I have so far:

def isSat(clauses,variable,n):
  if variable > n:
    if not contradiction(clauses):
      return 'satisfiable'
    if contradiction(clauses):
      return 'unsatisifable'
  clauses1 = simplification(clauses,variable)
  clauses2 = simplification(clauses,-variable)
  if not contradiction(clauses1):
    return isSat(clauses1,variable+1,n)
  if not contradiction(clauses2):
    return isSat(clauses2,variable+1,n)
  return 'unsatisfiable'

essentially I need to, starting from the first variable, set it to true and false, and check both cases for contradictions. Then, for each case that has no contradictions, recursively test both cases for the next variable. It will return satisfiable if it reached the last variable with no contradictions. (It only needs to return yes or no)

Answer 1

Turns out the problem was in a rare edge case where the same variable appeared twice in a clauses I.E. [9,-5,10,3,9]. In this case my simplification function would only remove one instance of the variable. Should not have assumed only 1 instance of a variable per clause