p-sat-crap.py

#!/usr/bin/env python

#disclaimer: this code as a SAT solver is pure crap. Don't waste your time.

#prettify http://stackoverflow.com/questions/1151658/python-hashable-dicts
class hashdict(dict):
  def __hash__(self):
    return hash(tuple(sorted(self.items())))


def sat(fla):
  '''receives a formula as a conjunctive list of disjuntive lists of atoms'''
  '''an atom is a possibly negated variable, examples: "-x", "es"'''
  res = [{}]
  for dis in fla:
    nres = []
    for var in dis:
      for sol in res:
          sol2 = hashdict(sol) 
          if (var[0]=='-' and var[1:] in sol and sol[var[1:]] == False):
            nres.append(sol2)
          elif (var[0]!='-' and var in sol and sol[var] == True):
            nres.append(sol2)
          elif (var[0]=='-' and var[1:] not in sol):
            sol2[var[1:]]=False
            nres.append(sol2)
          elif (var[0]!='-' and var not in sol):
            sol2[var]=True
            nres.append(sol2)
    res = set(nres)
  return res
      
if __name__ == "__main__":
  print(sat([['a','b','c'],['a','b','-c'],['a','-b','c'],['a','-b','-c'],
    ['-a','b','c'],['-a','b','c'],['-a','b','-c'],['-a','-b','c'],
    ['-a','-b','c']]))