Tag Archives: HornSAT

Greedy HornSAT in Python

Consider this logic puzzle:

If Mr. Smith has a dog, then Mrs. Brown has a cat.
If Mr. Jones has a dog, then he has a cat too.
If Mr. Smith has a dog and Mr. Jones has a cat, then Mrs. Peacock has a dog.
If Mrs. Brown and Mr. Jones share a pet of the same species, then Mr. Smith has a cat
All the men have dogs.

What can we say about who has what kind of pet?

We can encode the problem as Boolean variables. We write s, j, b, p for Boolean variables that are true if Smith, Jones, Brown, or Peacock respectively have a dog, and S, J, B, P for Boolean variables that are true if they have a cat. The puzzle can then be exressed as the following logical formula:

\(
\begin{matrix}
(s & \Rightarrow & B) & \land \\
(j & \Rightarrow & J) & \land \\
((s \land J) & \Rightarrow & p) & \land \\
((b \land j) & \Rightarrow & S) & \land \\
((B \land J) & \Rightarrow & S) & \land \\
& & (s) & \land \\
& & (j). &
\end{matrix}
\)

A formula that is a conjunction of implications in which no variable is complemented is called a Horn formula. To solve the puzzle, we need to find a satisfying truth assignment for the variables in the formula. While the problem of Boolean Satisfiability (SAT) is in general intractable, Boolean satisfiability for Horn clauses – HornSAT – can be solved in linear time using a greedy algorithm.

The algorithm works as follows:

  1. Make a set of truth assignments for the variables, starting with them all set to False
  2. Make a set W of all of the variables that appear on the right hand side of an empty implication
  3. While W is not empty:
    1. Remove an arbitrary element v from W
    2. Set v to True
    3. For each clause c where v appears on the left hand side:
      1. Delete v from the left hand side of c
      2. If this makes c and empty implication, add the variable on the right hand side of c to W, unless it is already there
  4. Return the set of truth assignments

Here is the implementation in Python:

def greedy_hornsat(variables, clauses):
    """Take a list of variables and horn clauses and return a truth assignment
    to the variables that satisfies all of them"""
    assignment = dict((v, False) for v in variables)
    working = set(t[1] for t in clauses if not len(t[0]))
    while working:
        v = working.pop()
        assignment[v] = True
        vclauses = [ c for c in clauses if v in c[0]]
        for vclause in vclauses:
            vclause[0].remove(v)
            if not vclause[0]:
                working.add(vclause[1])

    return assignment

An example program using the puzzle above:

def main():
    variables = ['s', 'j', 'b', 'p', 'S', 'J', 'B', 'P']
    clauses = [(['s'], 'B'),
            (['j'], 'J'),
            (['s', 'J'], 'p'),
            (['b', 'j'], 'S'),
            (['B', 'J'], 'S'),
            ([], 's'),
            ([], 'j')]
    assignment = greedy_hornsat(variables, clauses)
    print(assignment)

if __name__ == '__main__':
    main()

The output:

{'b': False, 'P': False, 'J': True, 'j': True, 'S': True, 'p': True, 's': True, 'B': True}

So we know that Mr. Jones and Mr. Smith both have a dog and a cat, Mrs. Brown has a cat, and Mrs. Peacock has a dog. Mrs. Brown may also have a dog, and Mrs. Peacock may also have a cat, but we don’t know those.

Reference: Notes for CS 170