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 is satisfiable: just set to true and to false. By contrast, the formula is “unsatisfiable” because it comes out false irrespective of what value you assign to .

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 is in 3CNF; the formula 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. is represented as:

("p", False)

A disjunctive clause is a set of literals. E.g. is represented as:

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

A CNF formula is a list of disjunctive clauses. E.g. 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.

Full code can be found here.

A year-old stack overflow question that I’m able to answer? This is like spotting Bigfoot. I’m going to assume access to nothing more than a spark context. Let’s start by parallelizing some familiar sentences.

corpus = sc.parallelize([
    "We're talking about practice, man.",
    "We're talking about practice.",
    "We ain't talking about the game."])

The first step is to tokenize our documents and cache the resulting RDD. In practice, by which I mean the game, we would use a real tokenizer, but for illustrative purposes I’m going to keep it simple and split on spaces.

tokenized_corpus = corpus \
    .map(lambda raw_text: raw_text.split()) \
    .cache()

Next we need to map words to distinct indices and pull the resulting dictionary into the driver.

local_vocab_map = tokenized_corpus \
    .flatMap(lambda token: token) \
    .distinct() \
    .zipWithIndex() \
    .collectAsMap()

Then we can broadcast the vocabulary-index map (and its size) back out to the workers:

vocab_map = sc.broadcast(local_vocab_map)
vocab_size = sc.broadcast(len(local_vocab_map))

Finally, we need to:
1) Convert each document into a dictionary of word counts
2) Replace the keys in the dictionary with their indices
3) Convert the dictionary into a vector

With the help of two imports we can do this in three calls to map:

from pyspark.mllib.linalg import SparseVector
from collections import Counter

term_document_matix = tokenized_corpus \
    .map(Counter) \
    .map(lambda counts: {vocab_map.value[token]: float(counts[token]) for token in counts}) \
    .map(lambda index_counts: SparseVector(vocab_size.value, index_counts))

Voila:

for vec in term_document_matix.collect():
    print vec

(10,[0,1,6,7,8],[1.0,1.0,1.0,1.0,1.0])
(10,[0,3,7,8],[1.0,1.0,1.0,1.0])
(10,[0,2,4,5,7,9],[1.0,1.0,1.0,1.0,1.0,1.0])

The practice rant turned fourteen today.