SAT Solvers¶
Overview¶
A SAT Solver is tool for finding solutions to problems that can be specified using propositional logic formulas.
Here’s an example from Delmar E. Searls.
Start with a problem statement, “If the tire is flat then I will have to remove it and take it to the gas station.”
Translate each basic statement to a variable so that P means “the tire is flat”, Q means “I have to remove the tire”, and R means “I have to take the tire to the gas station.
Next, write the statement in symbolic form: P → (Q ∧ R) and make a truth table that shows when the statements is satisfied:
P Q R P → (Q ∧ R) T T T T T T F F T F T F T F F F F T T T F T F T F F T T F F F T
Since there is at least one row that evaluates to True, we say the expression is satisfiable.
What a SAT solver does is determine whether an expression is satisfiable and will generate one, some, or all of the rows that evaluate to true.
Why Do We Care?¶
There are many otherwise difficult problems that can be expressed in propositional logic and computers have gotten good at solving them.
While the above example was simple, the problem grows exponentially with the number of variables. The amazing fact of the early 21st century is that a number of heuristics have been found that make the problem tractable for many practical examples, even ones with tens of thousands of variables.
One example is finding a layout to wire a printed circuit board in a way that doesn’t generate electrical interference.
Tools¶
A tool that is available to Pythonistas is pycosat which is itself a front-end for a PicoSAT which is a popular SAT solver written by Armin Biere in pure C.
The first step is to rewrite the expression into Conjunctive Normal Form (CNF) sometimes called a “product of sums”:
(¬P ∨ Q) ∧ (¬P ∨ R)
In pycosat, P is written as 1 because it is the first
variable, and ¬P is written as -1 using a negative
value to indicate negation. We pass in a list of tuples with
each disjunction was a separate tuple:
>>> pprint(list(pycosat.itersolve([(-1, 2), (-1, 3)])), width=20)
[[-1, 2, 3],
[-1, 2, -3],
[-1, -2, 3],
[-1, -2, -3],
[1, 2, 3]]
The Core Challenge¶
With a powerful SAT solver at you disposal, the remaining challenge is to express your problem in a way that pycosat can understand.
I wrote some utility functions that can help. For starters, we
want to write our expressions with symbols instead of numbers
and with ~ for negation instead of a minus sign:
>>> translate([['~P', 'Q'],['~P', 'R']])[0]
[(-1, 2), (-1, 3)]
Often, it is easier to express constraints in Disjunctive normal form
¬P ∨ (Q ∧ R)
and then convert to the CNF required by pycosat:
>>> from_dnf([['~P'], ['Q', 'R']])
[('~P', 'Q'), ('~P', 'R')]
Lastly, there is function, solve_all, that takes care of the round-trip between human readable and pycosat readable:
>>> cnf = from_dnf([['~P'], ['Q', 'R']])
>>> solve_all(cnf, True)
[['~P', 'Q', 'R'],
['~P', 'Q', '~R'],
['~P', '~Q', 'R'],
['~P', '~Q', '~R'],
['P', 'Q', 'R']]
It’s even more readable with humanistic variable names:
>>> cnf = from_dnf([['~FlatTire'], ['NeedToRemove', 'GotoGasStation']])
>>> solve_all(cnf, True)
[['~FlatTire', 'NeedToRemove', 'GotoGasStation'],
['~FlatTire', 'NeedToRemove', '~GotoGasStation'],
['~FlatTire', '~NeedToRemove', 'GotoGasStation'],
['~FlatTire', '~NeedToRemove', '~GotoGasStation'],
['FlatTire', 'NeedToRemove', 'GotoGasStation']]
Higher Level Convenience Functions¶
DNFs can be easy to reason about but are sometimes tedious to write-out.
I have some convenience functions that build a CNF directly from constraints expressed with quantifiers:
# Express that at least one of A, B, and C are true
>>> some_of(['A', 'B', 'C'])
[['A', 'B', 'C']]
# Express that at exactly one of A, B, and C is true
>>> one_of(['A', 'B', 'C'])
[('A', 'B', 'C'),
('~A', '~B'),
('~A', '~C'),
('~B', '~C')]
# Express that no more than one of A, B, and C are true
>>> Q(['A', 'B', 'C']) <= 1
[('~A', '~B'),
('~A', '~C'),
('~B', '~C')]
With these tools as primitives, it is easier to write higher level functions to express problem constraints in conjunctive normal form.
Sudoku Puzzles¶
Given a puzzle in this form:
8 6|4 3|
5 | | 7
| 2 |
---+---+---
32 | 8 | 5
8| 5 |4
1 | 7 | 93
---+---+---
| 4 |
9 | | 4
|6 7|2 8
We enter it in Python as a single string row major order:
s = ('8 64 3 5 7 2 '
'32 8 5 8 5 4 1 7 93'
' 4 9 4 6 72 8')
And expect the computer to solve it:
876|413|529
452|968|371
931|725|684
---+---+---
329|184|756
768|359|412
145|276|893
---+---+---
283|541|967
697|832|145
514|697|238
Code for the Sudoku Solver¶
from sat_utils import solve_one, one_of, basic_fact
from sys import intern
from pprint import pprint
n = 3
grid = '''\
AA AB AC BA BB BC CA CB CC
AD AE AF BD BE BF CD CE CF
AG AH AI BG BH BI CG CH CI
DA DB DC EA EB EC FA FB FC
DD DE DF ED EE EF FD FE FF
DG DH DI EG EH EI FG FH FI
GA GB GC HA HB HC IA IB IC
GD GE GF HD HE HF ID IE IF
GG GH GI HG HH HI IG IH II
'''
values = list('123456789')
table = [row.split() for row in grid.splitlines()]
points = grid.split()
subsquares = dict()
for point in points:
subsquares.setdefault(point[0], []).append(point)
# Groups: rows + columns + subsquares
groups = table[:] + list(zip(*table)) + list(subsquares.values())
del grid, subsquares, table # analysis requires only: points, values, groups
def comb(point, value):
'Format a fact (a value assigned to a given point)'
return intern(f'{point} {value}')
def str_to_facts(s):
'Convert str in row major form to a list of facts'
return [comb(point, value) for point, value in zip(points, s) if value != ' ']
def facts_to_str(facts):
'Convert a list of facts to a string in row major order with blanks for unknowns'
point_to_value = dict(map(str.split, facts))
return ''.join(point_to_value.get(point, ' ') for point in points)
def show(flatline):
'Display grid from a string (values in row major order with blanks for unknowns)'
fmt = '|'.join(['%s' * n] * n)
sep = '+'.join(['-' * n] * n)
for i in range(n):
for j in range(n):
offset = (i * n + j) * n**2
print(fmt % tuple(flatline[offset:offset+n**2]))
if i != n - 1:
print(sep)
for given in [
'53 7 6 195 98 6 8 6 34 8 3 17 2 6 6 28 419 5 8 79',
' 75 4 5 8 17 6 36 2 7 1 5 1 1 5 8 96 1 82 3 4 9 48 ',
' 9 7 4 1 6 2 8 1 43 6 59 1 3 97 8 52 7 6 8 4 7 5 8 2 ',
'67 38 921 85 736 1 8 4 7 5 1 8 4 2 6 8 5 175 24 321 61 84',
'27 15 8 3 7 4 7 5 1 7 9 2 6 2 5 8 6 5 4 8 59 41',
'8 64 3 5 7 2 32 8 5 8 5 4 1 7 93 4 9 4 6 72 8',
]:
cnf = []
# each point assigned exactly one value
for point in points:
cnf += one_of(comb(point, value) for value in values)
# each value gets assigned to exactly one point in each group
for group in groups:
for value in values:
cnf += one_of(comb(point, value) for point in group)
# add facts for known values in a specific puzzle
for known in str_to_facts(given):
cnf += basic_fact(known)
# solve it and display the results
result = facts_to_str(solve_one(cnf))
show(given)
print()
show(result)
print('=-' * 20)
Einstein Puzzle¶
Reportedly this puzzle is from Albert Einstein who is said to have remarked that fewer than 2% of the population can solve this puzzle (this is lore, neither fact is true).
Entities¶
- There are five houses in unique colors: Blue, green, red, white and yellow.
- In each house lives a person of unique nationality: British, Danish, German, Norwegian and Swedish.
- Each person drinks a unique beverage: Beer, coffee, milk, tea and water.
- Each person smokes a unique cigar brand: Blue Master, Dunhill, Pall Mall, Prince and blend.
- Each person keeps a unique pet: Cats, birds, dogs, fish and horses.
Constraints¶
- The Brit lives in a red house.
- The Swede keeps dogs as pets.
- The Dane drinks tea.
- The green house is on the left of the white, next to it.
- The green house owner drinks coffee.
- The person who smokes Pall Mall rears birds.
- The owner of the yellow house smokes Dunhill.
- The man living in the house right in the center drinks milk.
- The Norwegian lives in the first house.
- The man who smokes blend lives next to the one who keeps cats.
- The man who keeps horses lives next to the man who smokes Dunhill.
- The owner who smokes Blue Master drinks beer.
- The German smokes Prince.
- The Norwegian lives next to the blue house.
- The man who smokes blend has a neighbor who drinks water.
Goal¶
The question you need to answer is: “Who keeps fish?”
Solution Techniques¶
Christian Stigen Larsen has a nice write-up on how to solve this problem by hand
Instead, we’ll use a computer to determine all of the relationships:
['1 norwegian', '1 yellow', '1 cat', '1 water', '1 dunhill',
'2 dane', '2 blue', '2 horse', '2 tea', '2 blends',
'3 brit', '3 red', '3 bird', '3 milk', '3 pall mall',
'4 german', '4 green', '4 fish', '4 coffee', '4 prince',
'5 swede', '5 white', '5 dog', '5 root beer', '5 blue master']
The fish is in green house owned by the german who drinks coffee and smokes Prince.
Code for the Einstein Puzzle¶
from sat_utils import solve_one, from_dnf, one_of
from sys import intern
from pprint import pprint
houses = ['1', '2', '3', '4', '5' ]
groups = [
['dane', 'brit', 'swede', 'norwegian', 'german' ],
['yellow', 'red', 'white', 'green', 'blue' ],
['horse', 'cat', 'bird', 'fish', 'dog' ],
['water', 'tea', 'milk', 'coffee', 'root beer'],
['pall mall', 'prince', 'blue master', 'dunhill', 'blends' ],
]
values = [value for group in groups for value in group]
def comb(value, house):
'Format how a value is shown at a given house'
return intern(f'{value} {house}')
def found_at(value, house):
'Value known to be at a specific house'
return [(comb(value, house),)]
def same_house(value1, value2):
'The two values occur in the same house: brit1 & red1 | brit2 & red2 ...'
return from_dnf([(comb(value1, i), comb(value2, i)) for i in houses])
def consecutive(value1, value2):
'The values are in consecutive houses: green1 & white2 | green2 & white3 ...'
return from_dnf([(comb(value1, i), comb(value2, j))
for i, j in zip(houses, houses[1:])])
def beside(value1, value2):
'The values occur side-by-side: blends1 & cat2 | blends2 & cat1 ...'
return from_dnf([(comb(value1, i), comb(value2, j))
for i, j in zip(houses, houses[1:])] +
[(comb(value2, i), comb(value1, j))
for i, j in zip(houses, houses[1:])]
)
cnf = []
# each house gets exactly one value from each attribute group
for house in houses:
for group in groups:
cnf += one_of(comb(value, house) for value in group)
# each value gets assigned to exactly one house
for value in values:
cnf += one_of(comb(value, house) for house in houses)
cnf += same_house('brit', 'red')
cnf += same_house('swede', 'dog')
cnf += same_house('dane', 'tea')
cnf += consecutive('green', 'white')
cnf += same_house('green', 'coffee')
cnf += same_house('pall mall', 'bird')
cnf += same_house('yellow', 'dunhill')
cnf += found_at('milk', 3)
cnf += found_at('norwegian', 1)
cnf += beside('blends', 'cat')
cnf += beside('horse', 'dunhill')
cnf += same_house('blue master', 'root beer')
cnf += same_house('german', 'prince')
cnf += beside('norwegian', 'blue')
cnf += beside('blends', 'water')
pprint(solve_one(cnf))
Essential Utilities for Humanization¶
'Utility functions to humanize interaction with pycosat'
__author__ = 'Raymond Hettinger'
import pycosat # https://pypi.python.org/pypi/pycosat
from itertools import combinations
from functools import lru_cache
from sys import intern
def make_translate(cnf):
"""Make translator from symbolic CNF to PycoSat's numbered clauses.
Return a literal to number dictionary and reverse lookup dict
>>> make_translate([['~a', 'b', '~c'], ['a', '~c']])
({'a': 1, 'c': 3, 'b': 2, '~a': -1, '~b': -2, '~c': -3},
{1: 'a', 2: 'b', 3: 'c', -1: '~a', -3: '~c', -2: '~b'})
"""
lit2num = {}
for clause in cnf:
for literal in clause:
if literal not in lit2num:
var = literal[1:] if literal[0] == '~' else literal
num = len(lit2num) // 2 + 1
lit2num[intern(var)] = num
lit2num[intern('~' + var)] = -num
num2var = {num:lit for lit, num in lit2num.items()}
return lit2num, num2var
def translate(cnf, uniquify=False):
'Translate a symbolic cnf to a numbered cnf and return a reverse mapping'
# DIMACS CNF file format:
# http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html
if uniquify:
cnf = list(dict.fromkeys(cnf))
lit2num, num2var = make_translate(cnf)
numbered_cnf = [tuple([lit2num[lit] for lit in clause]) for clause in cnf]
return numbered_cnf, num2var
def itersolve(symbolic_cnf, include_neg=False):
numbered_cnf, num2var = translate(symbolic_cnf)
for solution in pycosat.itersolve(numbered_cnf):
yield [num2var[n] for n in solution if include_neg or n > 0]
def solve_all(symcnf, include_neg=False):
return list(itersolve(symcnf, include_neg))
def solve_one(symcnf, include_neg=False):
return next(itersolve(symcnf, include_neg))
############### Support for Building CNFs ##########################
@lru_cache(maxsize=None)
def neg(element) -> 'element':
'Negate a single element'
return intern(element[1:] if element.startswith('~') else '~' + element)
def from_dnf(groups) -> 'cnf':
'Convert from or-of-ands to and-of-ors'
cnf = {frozenset()}
for group in groups:
nl = {frozenset([literal]) : neg(literal) for literal in group}
# The "clause | literal" prevents dup lits: {x, x, y} -> {x, y}
# The nl check skips over identities: {x, ~x, y} -> True
cnf = {clause | literal for literal in nl for clause in cnf
if nl[literal] not in clause}
# The sc check removes clauses with superfluous terms:
# {{x}, {x, z}, {y, z}} -> {{x}, {y, z}}
# Should this be left until the end?
sc = min(cnf, key=len) # XXX not deterministic
cnf -= {clause for clause in cnf if clause > sc}
return list(map(tuple, cnf))
class Q:
'Quantifier for the number of elements that are true'
def __init__(self, elements):
self.elements = tuple(elements)
def __lt__(self, n: int) -> 'cnf':
return list(combinations(map(neg, self.elements), n))
def __le__(self, n: int) -> 'cnf':
return self < n + 1
def __gt__(self, n: int) -> 'cnf':
return list(combinations(self.elements, len(self.elements)-n))
def __ge__(self, n: int) -> 'cnf':
return self > n - 1
def __eq__(self, n: int) -> 'cnf':
return (self <= n) + (self >= n)
def __ne__(self, n) -> 'cnf':
raise NotImplementedError
def __repr__(self) -> str:
return f'{self.__class__.__name__}(elements={self.elements!r})'
def all_of(elements) -> 'cnf':
'Forces inclusion of matching rows on a truth table'
return Q(elements) == len(elements)
def some_of(elements) -> 'cnf':
'At least one of the elements must be true'
return Q(elements) >= 1
def one_of(elements) -> 'cnf':
'Exactly one of the elements is true'
return Q(elements) == 1
def basic_fact(element) -> 'cnf':
'Assert that this one element always matches'
return Q([element]) == 1
def none_of(elements) -> 'cnf':
'Forces exclusion of matching rows on a truth table'
return Q(elements) == 0