# 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]:

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