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:

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

- Delete

- Remove an arbitrary element
- 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