布尔SAT求解器递归

Question

我需要为家庭作业做一个SAT解算器。我的输入给出了n个变量x1、x2...xn和M子句，这些子句是文字的脱节，由列表ex表示。[-1,2,3,2，-3,1，-3]其中-1,3,2，-3指(~X1或X3)和(X2或~X3)。

我的计划是实现一个回溯解决方案，首先选择X1 = False，然后递归地检查每个变量的等式。

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

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。在这种情况下，我的简化函数只会删除变量的一个实例。不应该假设每个子句仅包含一个变量实例。