A really basic DPLL SAT solver

sat.py

import sys

# (a | b) & (~b | c)
# [[a, b], [~b, c]]
# [[1, 2], [-2, 3]]

# (a | b) & (~b | c) & (b)
# b is true
# (a | T) & (F | c) & (T)
# T & (c) & T
# (c)

def is_sat(cnf):
    "The empty formula is satisfied."
    return len(cnf) == 0

def has_empty(cnf):
    "An empty clause is unsatisifiable."
    return any(len(clause) == 0 for clause in cnf)

def find_units(cnf):
    "Make a list of all literals that appear in unit clauses"
    return [c[0] for c in cnf if len(c) == 1]

def prop(cnf, l):
    a = set()
    for lit in l:
        if lit in a or -lit in a:
            continue
        a.add(lit)
        cnf = [[l for l in clause if l != -lit]
               for clause in cnf
               if lit not in clause]
    return a, cnf

def pick_lit(cnf):
    return cnf[0][0]

def sat(cnf):
    a0 = set()
    # Propogate units
    units = find_units(cnf)
    while units:
        a, cnf = prop(cnf, units)
        a0 |= a
        units = find_units(cnf)
    # Check for unsatisfiable or satisfied
    if has_empty(cnf):
        return None
    elif is_sat(cnf):
        return a0
    # Guess with backtracking
    lit = pick_lit(cnf)
    a = sat(cnf + [[lit]])
    if a is not None:
        return a | a0
    a = sat(cnf + [[-lit]])
    if a is not None:
        return a | a0
    return None


cnf = [[1], [-1, 2]]
for line in sys.stdin.readlines():
    if line.startswith('c') or line.startswith('p'):
        continue
    cnf.append([int(x) for x in line.split()[:-1]])
print(cnf)
a = sat(cnf)
if a is None:
    print('UNSAT')
else:
    print('SAT')
    print(a)