Full code for solving SAT in Python

dpll

import seaborn as sns
import pandas as pd
import pylab as plt
import numpy as np
import itertools
import random
import time


def brute_force(cnf):
    literals = set()
    for conj in cnf:
        for disj in conj:
            literals.add(disj[0])
 
    literals = list(literals)
    n = len(literals)
    for seq in itertools.product([True,False], repeat=n):
        a = set(zip(literals, seq))
        if all([bool(disj.intersection(a)) for disj in cnf]):
            return True, a
 
    return False, None

def __select_literal(cnf):
    for c in cnf:
        for literal in c:
            return literal[0]
 
def dpll(cnf, assignments={}):
 
    if len(cnf) == 0:
        return True, assignments
 
    if any([len(c)==0 for c in cnf]):
        return False, None
    
    l = __select_literal(cnf)
 
    new_cnf = [c for c in cnf if (l, True) not in c]
    new_cnf = [c.difference({(l, False)}) for c in new_cnf]
    sat, vals = dpll(new_cnf, {**assignments, **{l: True}})
    if sat:
        return sat, vals
         
    new_cnf = [c for c in cnf if (l, False) not in c]
    new_cnf = [c.difference({(l, True)}) for c in new_cnf]
    sat, vals = dpll(new_cnf, {**assignments, **{l: False}})
    if sat:
        return sat, vals
 
    return False, None

def random_kcnf(n_literals, n_conjuncts, k=3):
    result = []
    for _ in range(n_conjuncts):
        conj = set()
        for _ in range(k):
            index = random.randint(0, n_literals)
            conj.add((
                str(index).rjust(10, '0'),
                bool(random.randint(0,2)),
            ))
        result.append(conj)
    return result

if __name__ == "main":

    brute_force_times = []
    dpll_times = []
    for n_literals in range(16):
        current_brute_force_times = []
        current_dpll_times = []
        for _ in range(100):
            n_conjuncts = random.randint(0, n_literals*6)
            s = random_kcnf(n_literals, n_conjuncts)
            start = time.time()
            brute_force(s)
            stop = time.time()
            current_brute_force_times.append(stop-start)
            start = time.time()
            dpll(s)
            stop = time.time()
            current_dpll_times.append(stop-start)
        brute_force_times.append(np.mean(current_brute_force_times))
        dpll_times.append(np.mean(current_dpll_times))
    
    df = pd.DataFrame(
        {'Number of literals': range(16),
         'Brute Force': brute_force_times,
         'DPLL': dpll_times
        }
    )
    
    sns.set()
    viz = df.plot(x='Number of literals')
    viz.set_ylabel("Time (Seconds)")
    plt.show()