Teaching myself about SAT solvers -- DPLL

dpll.py

import sys


def parse_cnf(infn):
    with open(infn, 'r') as f:
        inp = f.readlines()

    # print(inp)
    while inp:
        l = inp[0]
        inp = inp[1:]
        if l.startswith('c'):
            pass
        elif l.startswith('p'):
            # print(l)
            _, fmt, nvars, nclauses = l.split()
            assert fmt == "cnf"
            nvars = int(nvars)
            nclauses = int(nclauses)
            # print(fmt, nvars, nclauses)

            clause_data = [x for l in inp for x in l.split()]
            # print(clause_data)

            clauses = []
            for _ in range(nclauses):
                # print(clause_data)
                this_clause = clause_data[:clause_data.index('0')]
                clause_data = clause_data[clause_data.index('0') + 1:]
                clauses.append([int(x) for x in this_clause])

            # print(clauses)
            # print(clause_data)

            assert clause_data == [] or clause_data == ['%', '0']

            break
        else:
            assert False

    return nvars, clauses


def find_unit_clause(clauses):
    for i in range(len(clauses)):
        clause = clauses[i]
        if len(clause) == 1:
            return i, clause
    return None, None


def find_empty_clause(clauses):
    for clause in clauses:
        if len(clause) == 0:
            return True
    return False


def very_simple_dpll(clauses, vars_, assignments=[], lvl=0):
    indent = "\t" * lvl

    # print(f"{indent}clauses {clauses} assignments {assignments} vars {vars_}")

    unit_clause_i, unit_clause = find_unit_clause(clauses)
    while unit_clause:
        # print(f"{indent} found unit clause {unit_clause}")
        v = unit_clause[0]
        # assign
        assignments.append(v)
        vars_.remove(abs(v))
        clauses.pop(unit_clause_i)

        # propagate
        new_clauses = []
        for clause in clauses:
            if v in clause:
                # print(f"{indent} dropping {clause}")
                ...
            elif -v in clause:
                # print(f"{indent} dropping {-v} from {clause}")
                clause.remove(-v)
                new_clauses.append(clause)
            else:
                new_clauses.append(clause)
        clauses = new_clauses
        # print(f"{indent} clauses now {clauses}")

        unit_clause_i, unit_clause = find_unit_clause(clauses)

    # print(f"{indent}clauses {clauses} assignments {assignments} vars {vars_}")

    for v in set(vars_):
        is_pure = True
        pure_polarity = None

        for clause in clauses:
            if v in clause:
                if pure_polarity is None or pure_polarity > 0:
                    pure_polarity = 1
                else:
                    is_pure = False
                    break
            elif -v in clause:
                if pure_polarity is None or pure_polarity < 0:
                    pure_polarity = -1
                else:
                    is_pure = False
                    break

        # print(f"{indent} var {v} pure? {is_pure} polarity {pure_polarity}")

        if is_pure:
            # whee
            if pure_polarity is None or pure_polarity > 0:
                assignments.append(v)
            else:
                assignments.append(-v)
            vars_.remove(v)

            new_clauses = []
            for clause in clauses:
                if v in clause or -v in clause:
                    # print(f"{indent}  dropping {clause}")
                    ...
                else:
                    new_clauses.append(clause)
            clauses = new_clauses

    # print(f"{indent}clauses {clauses} assignments {assignments} vars {vars_}")

    if len(clauses) == 0:
        return True, sorted(set(assignments))

    if find_empty_clause(clauses):
        return False, None

    # have to assign a variable now
    chosen_var = sorted(vars_)[0]

    # print(f"{indent}choosing {chosen_var}")
    clauses_true = [list(clause) for clause in clauses]
    clauses_true.append([chosen_var])
    success, result_true = very_simple_dpll(clauses_true, set(vars_), list(assignments), lvl + 1)
    if success:
        return True, result_true

    # print(f"{indent}choosing {-chosen_var}")
    clauses_false = [list(clause) for clause in clauses]
    clauses_false.append([-chosen_var])
    success, result_false = very_simple_dpll(clauses_false, set(vars_), list(assignments), lvl + 1)
    if success:
        return True, result_false

    return False, None


def check_assignment(clauses, assignments):
    for clause in clauses:
        ok = False
        for var in clause:
            if var in assignments:
                ok = True
                break
        if not ok:
            return False
    return True


infn = sys.argv[1]
nvars, clauses = parse_cnf(infn)
# print("==========")
success, assignments = very_simple_dpll(clauses, set(range(1, nvars + 1)))
# print("==========")
print(success, assignments)
assert check_assignment(clauses, assignments)

# for instance in range(1000):
#     fn = f'uf20-0{instance + 1}.cnf'
#     print(fn)
#     nvars, clauses = parse_cnf(fn)
#     success, assignments = very_simple_dpll(clauses, set(range(1, nvars + 1)))
#     print(success, assignments)
#     assert success
#     assert check_assignment(clauses, assignments)

# for instance in range(1000):
#     fn = f'uf50-0{instance + 1}.cnf'
#     print(fn)
#     nvars, clauses = parse_cnf(fn)
#     success, assignments = very_simple_dpll(clauses, set(range(1, nvars + 1)))
#     print(success, assignments)
#     assert success
#     assert check_assignment(clauses, assignments)

# for instance in range(1000):
#     fn = f'uuf50-0{instance + 1}.cnf'
#     print(fn)
#     nvars, clauses = parse_cnf(fn)
#     success, assignments = very_simple_dpll(clauses, set(range(1, nvars + 1)))
#     print(success, assignments)
#     assert not success