Teaching myself about SAT solvers -- CDCL

cdcl.py

import sys


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

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

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

            clauses = []
            for _ in range(nclauses):
                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])

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

            break
        else:
            assert False

    return nvars, clauses


# implication graph = map of var -> either tuple ('assign', idx) or ('impl', [list of var])


def very_simple_cdcl(clauses, nvars):
    vars_ = set(range(1, nvars + 1))
    impl = {}
    assignments = []
    assumptions = []
    do_backjump = False

    while vars_:
        lvl = len(assumptions)
        indent = "\t" * lvl

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

        if do_backjump:
            chosen_var = abs(assignments[-1])
            # print(f"{indent}choosing {chosen_var} = False")
            do_backjump = False
        else:
            chosen_var = sorted(vars_)[0]
            vars_.remove(chosen_var)
            # print(f"{indent}choosing {chosen_var} = True")
            assignments.append(chosen_var)
            assumptions.append((chosen_var, list(assignments), set(vars_), dict(impl)))
        assert chosen_var not in impl
        impl[chosen_var] = ('assign', lvl)

        # unit propagate
        last_added_var = chosen_var
        new_impl_q = []
        while True:
            for clause in clauses:
                if last_added_var in clause or -last_added_var in clause:
                    # print(f"{indent} LOOKING {clause}")
                    is_unit = True
                    impl_var = None

                    for var in clause:
                        if var not in assignments:
                            if -var not in assignments:
                                # free var
                                if impl_var is not None:
                                    is_unit = False
                                    break
                                impl_var = var
                            else:
                                # the opposite is assigned, so this is a FALSE
                                ...
                        else:
                            # this value is assigned, this is a TRUE
                            is_unit = False
                            break

                    if impl_var is None:
                        is_unit = False

                    if is_unit:
                        # print(f"{indent} clause {clause} unit? {is_unit} free {impl_var}")

                        causes = []
                        for var in clause:
                            if var != impl_var:
                                causes.append(-var)
                        # print(f"{indent} assignment {impl_var} is implied by {causes}")
                        new_impl_q.append((impl_var, causes))

            # print(f"{indent} impl Q {new_impl_q}")

            if not new_impl_q:
                break

            impl_var, causes = new_impl_q.pop()
            if abs(impl_var) in vars_:
                vars_.remove(abs(impl_var))
            impl[impl_var] = ('impl', causes)
            assignments.append(impl_var)
            last_added_var = impl_var

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

        # look for conflicts
        for var in range(1, nvars + 1):
            if var in impl and -var in impl:
                # print(f"{indent} CONFLICT {var}")
                new_clause = list(set((-x for x in impl[var][1])) | set((-x for x in impl[-var][1])))
                # print(f"{indent}  -> {new_clause}")
                clauses.append(new_clause)

                if len(assumptions) == 0:
                    return False, None

                firstvar, assignments, vars_, impl = assumptions[-1]
                assumptions = assumptions[:-1]
                assignments = list(assignments)
                vars_ = set(vars_)
                impl = dict(impl)
                # print(f"{indent} backjumping to assignment of {firstvar}")
                assignments[-1] *= -1
                do_backjump = True
                break

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

    return True, sorted(set(assignments))


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)
success, assignments = very_simple_cdcl(clauses, nvars)
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_cdcl(clauses, nvars)
#     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_cdcl(clauses, nvars)
#     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_cdcl(clauses, nvars)
#     print(success, assignments)
#     assert not success