Dpll 1 | Python Fiddle

def listOflistCopy(l):
  # technical function
  # copy.deepcopy not available in classical python trinket
  # 
  result = []
  if len(l) == 0:
    return result
  else:
    for i in l:
      j = i[:] #shallow copy
      result.append(j)
    return result

def read_literal (lit):
  # a literal is a atom or the negation of an atom
  #-a is not a
  # a is atom a
  if lit[0] == '-':
    return [lit[1:], '-'] #[atom, polarity]
  else:
    return [lit, '+']

def evalue_clause(clause, assignement):
  if len(clause)==0:
    return False 
  else:
    atom = read_literal(clause[0])[0]
    polarity = read_literal(clause[0])[1]
    if atom in assignement:
      if (assignement[atom] and polarity=='+'):
        return True
      elif ((not assignement[atom]) and polarity=='-'):
        return True
      else:
        return evalue_clause(clause[1:], assignement)
    else:
      return -1 #assignement does not allow to evaluate clause

class Cnf:
  def create_cnf(self, file):
    nf = []
    dict1 = {} # or counting variable occurences
    dict2 = {} #for counting literal occurences
    for line in open(file):
      clause = []
      separator = ' '
      line = line.split(separator)
      if (len(line) == 1 and line[0]=='\n'): #would be an empty line
        return [nf, dict1, dict2]
      for i in line:
        if i != '/n': 
          literal = read_literal(i.strip())
          clause.append(i.strip()) #add literal  in clause
          key1 =  literal[0] #add variable name as key in dictionnary 
          if key1 in dict1:
            dict1[key1] = dict1[key1] + 1
          else:
            dict1[key1] = 1
          key2 = i.strip()
          if key2 in dict2:
            dict2[key2] = dict2[key2] + 1
          else:
            dict2[key2] = 1
      nf.append(clause)
    return [nf, dict1, dict2]
  ####### 
  def __init__(self, file=None):
    if file != None:
      p = self.create_cnf(file)
      self.normalForm = p[0]
      self.varsOccurences = p[1]
      self.litsOccurences = p[2]
      self.vars = sorted(p[1].keys())
    else:
      self.normalForm = []
      self.varsOccurences = {}
      self.litsOccurences = {}
      self.vars = []
  ######
  def copy(self):
    c = Cnf()
    c.normalForm = listOflistCopy(self.normalForm)
    c.varsOccurences = self.varsOccurences.copy()
    c.litsOccurences= self.litsOccurences.copy()
    c.vars = self.vars[:] #copy
    return c
  ######  
  def evalue(self, assignement):
    nf = self.normalForm
    if (not nf):
      return False
    elif len(nf)==0:
      return True #empty conjunction is True
    else:
      for clause in nf:
        e=evalue_clause(clause, assignement)
        if (not e) or e== -1:
          break
      return e
  ######
  def assignSimplify(self, var, boolean):
  #when variable var is assigned to True
  #all clauses containing var can be removed and
  # not var can be removed froml all clauses
  #method will return a copy  after simplification
    result = []
    c =  Cnf()
    nf = listOflistCopy(self.normalForm)
  # need a deep copy not to modify input cnf
    if boolean:
      for clause in nf:
        if var in clause:
          continue #clause is removed
        elif ('-' + var) in clause: 
          clause.remove('-' +var)
          result.append(clause)
        else: #var not in clause:
          result.append(clause)
    else:
    # var is negative polarity
      for clause in nf:
        if ("-" + var) in clause:
          continue #claused is removed
        if var in clause: 
          clause.remove(var)
          result.append(clause)
        else: # ("-" + var) not in clause:
          result.append(clause)
    #Now recompute dictionaries and list of variable
    d1={}
    d2={}
    for clause in result:
      if len(clause) ==0: # an empty clause is False
        result = [[]]
        break
      else:
        for i in clause:
          literal = read_literal(i.strip())
          key1 =  literal[0]
          key2 = i
          if key1 in d1:
            d1[key1] = d1[key1] + 1
          else:
            d1[key1] = 1
          if key2 in d2:
            d2[key2] = d2[key2] + 1
          else:
            d2[key2] = 1
    c.normalForm = result
    c.varsOccurences = d1
    c.litsOccurences = d2
    c.vars = sorted(d1.keys())
    return c
###################################    
  def assignSimplifyMultiple(self, assignment):
    c = self 
    for i in assignment:
      c = c.assignSimplify(i, assignment[i]) 
    return c
#################################
  def pureLiterals(self):
    positif = []
    negatif = []
    for l in self.litsOccurences:
      if read_literal(l)[1] == '+':
        positif.append(read_literal(l)[0])
      elif read_literal(l)[1] == '-':
        negatif.append(read_literal(l)[0])
    purePositif = []
    pureNegatif = []
    #print ('positif', positif)
    #print ('negatif', negatif)
    for i in positif:
      if i not in negatif:
        purePositif.append(i)
    for j in negatif:
      if j not in positif:
        pureNegatif.append(j)
    return [purePositif, pureNegatif]

def naive(cnf, assignement={}):
  vars = cnf.vars
  nf = cnf.normalForm
  if len(nf)==0: #empty cnf evalue to true
    return assignement
  elif len(nf[0])==0: #if cnf contains an empty clause, it evalues to False
    return False
  else:
    v= vars[0]
    assignement[v] = True #assign next var to True
    simplified = cnf.assignSimplify(v, True)
    tmp = naive(simplified, assignement)
    if tmp == False:
      assignement[v] = False
      simplified = cnf.assignSimplify(v, False)
      tmp = naive(simplified, assignement)  
    return tmp

def firstUnitClause(nf):
  assignement = {}
  for clause in nf:
    if len(clause)== 1: # clause has only one literal
      lit = read_literal(clause[0])
      if lit[1]=='+':
        assignement[lit[0]] = True
      else:
        assignement[lit[0]] = False
      break
  return assignement

def unitPropagation(cnf, assignment= {}):
  cond = True
  c= cnf.assignSimplifyMultiple(assignment)
  nf1 = c.normalForm
  a = firstUnitClause(nf1)
  if a == {}: # no unit clause found
    return [c, assignment]
  else:
    assignment.update(a)
    return unitPropagation(c,a)

def pureLiteralsElimination(simplified, assignement):
  positif = simplified.pureLiterals()[0]
  negatif = simplified.pureLiterals()[1]
  for i in positif:
    assignement[i] = True
  for j in negatif:
    assignement[j] = False

def dlpp_0(cnf):
  return dlpp(cnf, {})

def dlpp(cnf, assignement={}):
  vars = cnf.vars
  nf = cnf.normalForm
  #print(assignement)
  if len(nf)==0: #empty cnf evalue to true
    return assignement
  elif len(nf[0])==0: #if cnf contains an empty clause, it evalues to False
    #print ("assignement efore false", assignement)
    return False
  else:
    save_assignement = assignement.copy()
    v= vars[0]
    assignement[v] = True #assign next var to True
    simplified = cnf.assignSimplify(v, True)
    unitResult = unitPropagation(simplified, assignement)
    simplified = unitResult[0]
    #assignement.update(unitResult[1]) 
    pureLiteralsElimination(simplified, assignement) #no needs to return assignment, its passed by ref
    tmp = dlpp(simplified, assignement)
    if tmp == False:
      assignement = save_assignement #backtrack for assignement too
      assignement[v] = False
      #print("assign", v, False, assignement)
      unitResult= unitPropagation(cnf, assignement)
      simplified = unitResult[0]
      #assignement.update(unitResult[1])
      pureLiteralsElimination(simplified, assignement) #no needs to return assignment, its passed by ref
      tmp = dlpp(simplified, assignement)  
    return tmp

cnf1 = Cnf('cnf1') #false
cnf2 = Cnf('cnf2') #true
cnf4 = Cnf('cnf4') #true
cnf5 = Cnf('cnf5')# true with 1 2 -3 -4 -5 -6 7 8 -9 10 -11 -12 -13 -14 -15 -16 -17 18 -19 20 21 22 -23 -24 -25 26 -27 28 29 -30
cnf6 = Cnf('cnf6') #true with 1 2 -3 4
cnf7 = Cnf('cnf7') # true with # 1 -2 -3 -4 -5 6 -7 8 9 10
cnf8 = Cnf('cnf8') #false
cnf9 = Cnf('cnf9') #true  -1 -2 3 -4 -5 -6 7 -8 9 10 -11 -12 -13 14 -15
cnf10 = Cnf('cnf10') #false
cnf11 = Cnf('cnf11')

#print('check naive 1', not naive(cnf1))
#print('check naive 2', cnf2.evalue(naive(cnf2)))
#print('check naive 4', cnf4.evalue(naive(cnf4)))
#print('check naive 6', cnf6.evalue(naive(cnf6)))
#print('check naive 7', cnf7.evalue(naive(cnf7))) #
#print('check naive 8', not naive(cnf8))
#print('check naive 9', cnf9.evalue(naive(cnf9)))

#print('check dpll 1', not dlpp_0(cnf1)))
#print('check dpll 2', cnf2.evalue(dlpp_0(cnf2)))
#dlpp(cnf1)
#dlpp(cnf2)
#print('check dpll 4', cnf4.evalue(dlpp_0(cnf4)))
#print('check dpll 6', cnf6.evalue(dlpp_0(cnf6)))
#print('check dpll 7', cnf7.evalue(dlpp_0(cnf7))) #
#print('check 8', not dlpp_0(cnf8))
#print('check 9', cnf9.evalue(dlpp_0(cnf9)))
#print(dlpp_0(cnf9))

#unitClauses(f, {"3": True })
nf = [['-12', '9'], ['-12'], ['9', '-5'], ['4', '-8', '-14'], ['14', '4'], ['-6', '5'], ['-9'], ['5', '12', '-8'], ['6', '-9', '-5'], ['-6', '5'], ['-6'], ['4', '-8', '8'], ['6', '-6'], ['-14'], ['8'], ['7', '14', '9'], ['-4', '-14', '7'], ['7', '-5'], ['-8'], ['9'], ['-5', '-6', '5'], ['5'], ['-4', '-7', '-8'], ['12', '-5', '4'], ['-14', '-8'], ['5', '7', '-6']]

print(cnf11.pureLiterals())

Python Fiddle

Python Cloud IDE