DPLL algorithm for solving 3-SAT. I made this to visualise how the algorithm works. In the backtracking search, variable selection is done by lowest entropy score, domain value [true,false] ordering is done by choosing the value which satisfies the most clauses first.

dpll.py

import random
import math

def randToVar(val, vars):
    val -= vars
    if val >= 0:
        val += 1
    return val

def randClause(vars):
    vals = random.sample(range(0,vars*2), 3)
    for i in range(0,len(vals)):
        vals[i] = randToVar(vals[i], vars)
        
    return vals


def randSat(vars, clauses):
    sat = []
    for i in range(0,clauses):
        sat.append(randClause(vars))
    return sat

def getvars(sat):
    vars = set()
    for cl in sat:
        for v in cl:
            vars.add(v)
    return vars
    
def truth(v):
    if v > 0:
        return 'True'
    else:
        return 'False'
        
def assign(v):
    print('Set ' + str(abs(v)) + ' to ' + truth(v))

def unassign(v):
    print('Unassign ' + str(abs(v)) + ' (' + truth(v) + ')')
    
def makeGuess(v):
    print('Guess ' + str(abs(v)) + ' = ' + truth(v))
    #return
    #print stack:
    sb = []
    global stack
    for p in stack:
        v = p[0]
        sb.append(str(v))
    print('['+','.join(sb)+']')
    
    
def assignsat(sat, v):
    newsat = []
    for cl in sat:
        if v in cl:
            pass
        elif -v in cl:
            cl2 = cl[:]
            cl2.remove(-v)
            newsat.append(cl2)
        else:
            newsat.append(cl)
    return newsat
    
def computepn(sat, v):
    v = abs(v)
        
    p = 0
    n = 0
    for cl in sat:
        pos = v in cl
        neg = -v in cl
        if pos and not neg:
            p += 1
        elif neg and not pos:
            n += 1
    return p, n


def entropy(sat, v):
    p, n = computepn(sat,v)

    if p == 0 or n == 0:
        return 0
        
    r1 = p / (p+n)
    r2 = 1 - r1
    return -(r1*math.log2(r1) + r2*math.log2(r2))
        
    

def selectUnassignedVariable(sat):
    bestVar = 0
    lowestValue = 1000
    vars = sorted(filter(lambda v : v > 0, getvars(sat)))
    for v in vars:
        value = entropy(sat, v)
        if value < lowestValue:
            bestVar = v
            lowestValue = value
    return bestVar
    
def orderDomainValues(sat, v):
    p, n = computepn(sat, v)
    v = abs(v)
    if p > n:
        return v
    else:
        return -v
    
    
#stack contains [v,domain,cnf]
stack = []
def dplliteration(sat):
    global stack

    #Early Termination
    if len(sat) == 0:
        return True

    #Early Termination
    for cl in sat:
        if len(cl) == 0:
            sat =  backtrack()
            if sat == None:
                return False
            else:
                return sat
            
    #Pure Symbol Heuristic
    for v in getvars(sat):
        pure = True
        for i in range(0,len(sat)):
            cl = sat[i]
            if v in cl:
                pass
            elif -v in cl:
                pure = False
                break
        if pure:
            assign(v)
            return assignsat(sat, v)
            
    #Unit Clause Heuristic
    for i in range(0,len(sat)):
        cl = sat[i]
        if len(cl) == 1:
            v = cl[0]
            
            assign(v)
            return assignsat(sat, v)
           
    v = selectUnassignedVariable(sat)
    v = orderDomainValues(sat, v)
    domain = [-v]
    global stack
    stack.append([v, domain, sat])
    makeGuess(v)
    return assignsat(sat,v)
    
def backtrack():
    global stack
    while len(stack) > 0:
        p = stack.pop()
        domain = p[1]
        unassign(p[0])
        sat = p[2]
        if len(domain) > 0:
            v = domain[0]
            domain = domain[1:]
            stack.append([v, domain, sat])
            makeGuess(v)
            return assignsat(sat, v)
    return None
    
    
sat = randSat(3, 30)
print(sat)
while True:
    s = input()
    sat = dplliteration(sat)
    print(sat)
    if sat == True or sat == False:
        break