solving SAT in python

SAT is hard, but there are algorithms that tend to do okay empirically. I recently learned about the Davis-Putnam-Logemann-Loveland (DPLL) procedure and rolled up a short Python implementation.

(I can’t get no) satisfaction

A boolean formula is called “satisfiable” if you can assign truth values to the underlying atoms in such a way that the entire formula comes out true. For example, the formula $p \land \lnot q$ is satisfiable: just set $p$ to true and $q$ to false. By contrast, the formula $p \land \lnot p$ is “unsatisfiable” because it comes out false irrespective of what value you assign to $p$ .

The general problem – does a satisfying assignment exist for a given formula – is called boolean satisfiability (SAT). It turns out that solving SAT is equivalent to solving the restricted problem of 3SAT. This makes representation easier so I focused on that. The problem of 3SAT is the same, except that we only consider formulae in 3CNF (conjunctive normal form). That is, formulae that are conjunctions where every conjunct is a disjunction of three literals. For example, the formula $(p \lor \lnot q \lor r) \land (p \lor q \lor \lnot s)$ is in 3CNF; the formula $(p \lor \lnot q \land r) \lor (p \lor \lnot s)$ is not.

John Franco and John Martin have written extensively on the history of SAT, which goes as far back as Aristotle. The problem received attention from medieval, enlightenment, and early analytic philosophers. Modern computational approaches emerged in the middle of the last century. The DPLL procedure was published in 1962 (here’s the original paper). Its core ideas remain important ingredients in modern SAT solvers.

representation

After a brief and irritating foray down the OOP path, I decided to use raw types to represent everything. My code uses the following conventions:

A literal is a tuple consisting of a name and a sign. E.g. $\lnot p$ is represented as:

("p", False)

A disjunctive clause is a set of literals. E.g. $p \lor \lnot q \lor r$ is represented as:

{("p", True), ("q", False), ("r", True)}

A CNF formula is a list of disjunctive clauses. E.g. $(p \lor \lnot q) \land (p \lor r)$ is represented as:

[{("p", True), ("q", False)}, {("p", True), ("r", True)}]

the naive approach

The simplest way to solve sat is to try everything. Given a single assignment (represented as a set of literals), we can determine if it satisfies the formula by testing whether it intersects with every conjunct. To test if the formula is satisfiable, we iterate over all assignments, testing each as we go.

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

davis-putnam-logemann-loveland

The DPLL procedure is a recursive search algorithm. The base cases are those of an empty conjunct, which is true, and a conjunct containing an empty disjunct, which is false. (If you find the latter off-putting read this explanation). The recursion case then deals with a non-empty CNF formula that has no empty clauses. We pick an arbitrary literal and set it to true. This means that all conjuncts containing the literal drop out, and all conjuncts containing its negation have its negation removed. Then we recurse. If this doesn’t result in a satisfying assignment, we set the same literal to false and repeat the same procedure.

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

experiments

I used the following code to generate random 3CNF formulae:

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

I then compared the performance of the brute force approach and DPLL over various numbers of literals. Each scores is averaged over one hundred random formulae.

pydpll

Full code can be found here.