布尔SAT求解器递归

Question

我需要做一个SAT求解器作为作业。我的输入是n个变量x1,x2...xn，还有M个子句，这些子句是字面量的析取，表示为一个列表的列表，比如[[−1,2,3],[2,−3],[1,−3]]，其中[-1,3]表示(~X1或X3)，而(X2或~X3)则是(2,−3)。

我的计划是实现一个回溯算法，首先选择X1为假，然后递归检查其他变量的方程。

我现在的问题是如何设置递归。我有两个函数，一个是检查程序中的矛盾，另一个是根据选择的变量的真值来简化表达式。

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  

我希望从X1开始，递归地检查到Xn，如果发现矛盾就停止这个过程。非递归的解决方案也可以。

编辑：这是我目前的进展：

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'

基本上，我需要从第一个变量开始，将它设置为真和假，然后检查这两种情况是否有矛盾。对于每种没有矛盾的情况，递归测试下一个变量的两种情况。如果在没有矛盾的情况下到达最后一个变量，就返回可满足（只需要返回是或否）。

Answer 1

原来问题出在一个很少见的情况，就是同一个变量在一个条件里出现了两次，比如说[9,-5,10,3,9]。在这种情况下，我的简化函数只会去掉其中一个变量的出现。不能假设每个条件里只有一个变量。