- Areas we work in
- Software & Systems Engineering
- Big Data & Analytics
- Cybersecurity
- Missile Defense
- Information Technology
- Always looking for good people!
15-Peg Solitaire or Tricky Triangle¶
15-Peg Solitaire Rules¶
- Start with a single empty hole
- Remove pegs with “checkers jumps”
- Over immediate neighbor
- Into empty hole
- Win by clearing the board down to a single peg
- No legal move and multiple pegs remaining loses
- Mostly a way to kill time and keep kids amused
In [1]:
'''
0
1 2
3 4 5
6 7 8 9
A B C D E
'''
NEIGHBORS = [
[ 0, 1, 3], [0, 2, 5],
[ 1, 3, 6], [1, 4, 8],
[ 2, 4, 7], [2, 5, 9],
[ 3, 4, 5], [3, 6, 10], [3, 7, 12],
[ 4, 7, 11], [4, 8, 13],
[ 5, 8, 12], [5, 9, 14],
[ 6, 7, 8],
[ 7, 8, 9],
[10, 11, 12],
[11, 12, 13],
[12, 13, 14],
]
Candidate Approaches¶
- Depth-First Search (DFS)
- Breadth-First Search (BFS)
- Work backward from a winning board
- Bidirectional search
In [2]:
%%time
import copy
def depth_first_search(board):
def loop(b):
if b.count(True) == 1: loop.winners += 1
else:
can_move = False
for n in NEIGHBORS:
for i, j, k in [n, reversed(n)]:
if b[i] and b[j] and not b[k]: # legal move?
can_move = True
bnew = copy.copy(b)
bnew[i] = bnew[j] = False
bnew[k] = True
loop(bnew)
if not can_move: loop.losers += 1
loop.winners = loop.losers = 0
loop(board)
print(f'winners: {loop.winners}', f'losers: {loop.losers}', sep='\n')
depth_first_search([False, *[True] * 14])
How might we optimize?¶
- Exploit 3-fold rotational symmetry
- Memoization to deal with duplication
- But let’s go another direction …
Satisfiability Solver¶
- Given an arbitrary Boolean formula
- Does a variable assignment exist that makes the whole formula true?
- $(x_1\lor\lnot x_2\lor\lnot x_3)\land(\lnot x_4\lor x_5\lor\lnot x_6)\land\cdots$
- SMT or Satisfiability Modulo Theories
- higher-level languages on top of Boolean “assembly language”
- Declarative paradigm
- Declare what you want
- Let the machine figure it out
In [3]:
from z3 import *
def a_AND_NOTa():
a = Bool('a')
s = Solver()
s.add(a, Not(a))
if s.check() == unsat:
print('Phew! The universe is still sane.')
else:
print('All bets are off.')
a_AND_NOTa()
DeMorgan’s Theorem¶
$$\Huge{ \lnot (p\land q)\iff(\lnot p\lor\lnot q) \\ \quad \\ \lnot(p\lor q)\iff(\lnot p\land\lnot q) }$$In [4]:
from z3 import *
def check_demorgans_theorem():
p, q = Bools('p q')
demorgan1 = And(p, q) == Not( Or(Not(p), Not(q)))
demorgan2 = Or (p, q) == Not(And(Not(p), Not(q)))
s = Solver()
s.add(Or(Not(demorgan1), Not(demorgan2))) # why not?
if s.check() == unsat:
print('DeMorgan’s theorem holds')
else:
print('Oops')
print(s.model())
check_demorgans_theorem()
In [5]:
from z3 import *
def system_of_linear_equations():
x, y, z = Reals('x y z')
s = Solver()
# https://en.wikipedia.org/wiki/System_of_linear_equations
s.add(3*x + 2*y - z == 1)
s.add(2*x - 2*y - -4*z == -2)
s.add( -x + y/2 - z == 0)
if s.check() == sat:
print(s.model())
else:
print('No solution')
system_of_linear_equations()
Back to Cracker Barrel …¶
Board Representation¶
- Board states will be a bit vector of length 15
- Each bit is set if a peg is in that position, or clear otherwise
- A successful game has
- the start board
- plus the boards that result from 13 jumps
In [6]:
from z3 import *
HOLES = 15
Hole = [BitVecVal(1 << i, HOLES) for i in range(HOLES)]
Board = [BitVec(f'board_{i}', HOLES) for i in range(HOLES - 1)]
Board and Hole live in the SMT world¶
- So we must test them in hypothetical terms
In [7]:
def used(b, h): return Board[b] & Hole[h] == Hole[h]
# important: capital-N Not, i.e., z3.Not, rather than Python not
def empty(b, h): return Not(used(b, h))
# in future perfect tense: hole h will not have changed from p to q
def unchanged(p, q, h): return used(p, h) == used(q, h)
Describing a legal move¶
- For a peg in hole i to jump j and land in k
- Prior board p must have i and j used but k empty.
- Result board q must have i and j empty with k used.
- All other holes must remain unchanged between p and q.
In [8]:
def valid(p, q, i, j, k):
return And(
used(p, i), empty(q, i),
used(p, j), empty(q, j),
empty(p, k), used(q, k),
*[unchanged(p, q, h) for h in range(HOLES) if h not in [i, j, k]])
Account for adjacency¶
- Legal jumps require both
- valid hole states, and
- neighboring holes
In [9]:
def legal_transition(p, q):
return Or(
[valid(p, q, *l)
for n in NEIGHBORS
for l in [n, reversed(n)]])
In [10]:
winning_model = None
smt2 = None
def solve_tricky_triangle():
s = Solver()
for i in range(HOLES - 2):
s.add(legal_transition(i, i+1))
s.add(empty(0, 0))
if s.check() == sat:
global winning_model, smt2
winning_model = s.model()
smt2 = s.to_smt2()
else:
print('Failed to solve')
In [11]:
def show_board(b):
def binary_lsb_first(b):
return f'{{:0{HOLES}b}}'.format(b.as_long())[::-1]
s = binary_lsb_first(b)
j = 0
for i in range(1, 6):
leftpad = ' ' * (5 - i)
print(leftpad, ' '.join(s[j:j + i]), sep='')
j = j + i
In [12]:
solve_tricky_triangle()
if winning_model:
show_board(winning_model[Board[0]])
print()
show_board(winning_model[Board[1]])
In [13]:
if winning_model:
show_board(winning_model[Board[1]])
print()
show_board(winning_model[Board[2]])
In [14]:
if winning_model:
show_board(winning_model[Board[2]])
print()
show_board(winning_model[Board[3]])
In [15]:
if winning_model:
show_board(winning_model[Board[3]])
print()
show_board(winning_model[Board[4]])
In [16]:
if winning_model:
show_board(winning_model[Board[4]])
print()
show_board(winning_model[Board[5]])
In [17]:
if winning_model:
show_board(winning_model[Board[5]])
print()
show_board(winning_model[Board[6]])
In [18]:
if winning_model:
show_board(winning_model[Board[6]])
print()
show_board(winning_model[Board[7]])
In [19]:
if winning_model:
show_board(winning_model[Board[7]])
print()
show_board(winning_model[Board[8]])
In [20]:
if winning_model:
show_board(winning_model[Board[8]])
print()
show_board(winning_model[Board[9]])
In [21]:
if winning_model:
show_board(winning_model[Board[9]])
print()
show_board(winning_model[Board[10]])
In [22]:
if winning_model:
show_board(winning_model[Board[10]])
print()
show_board(winning_model[Board[11]])
In [23]:
if winning_model:
show_board(winning_model[Board[11]])
print()
show_board(winning_model[Board[12]])
In [24]:
if winning_model:
show_board(winning_model[Board[12]])
print()
show_board(winning_model[Board[13]])
A peek at the “assembly language”¶
In [25]:
smt2_lines = None
if smt2:
smt2_lines = str(smt2).splitlines()
print('\n'.join(smt2_lines[0:25]))
In [26]:
if smt2_lines: print('\n'.join(smt2_lines[25:50]))
In [27]:
if smt2_lines: print('\n'.join(smt2_lines[50:75]))
In [28]:
if smt2_lines: print('\n'.join(smt2_lines[1250:1262]))
Where else can we try this?¶
Turing Machine: Formal Definition¶
$\LARGE{M = (Q, \Sigma, q_0, F, \delta)}$
where
$Q$ is a finite set of states
$\Sigma$ is the finite tape alphabet
$q_0$ is the initial state
$F\subseteq Q$ is the set of final states
$\delta\subseteq(Q\times\Sigma)\times(Q\times\Sigma\times\{L,N,R\})$ is the transition function
Turing Machine Rules¶
At each step of the computation:
- Each tape square records exactly one symbol, $\sigma_A\in\Sigma$
- $M$ is in exactly one state $q_A\in Q$
- Tape head scans exactly one square
- $M$ reads $\sigma_A$ and consults $\delta$ for which …
- symbol $\sigma_B$ to write to the current tape square,
- direction (Left, None, or Right) to move the tape head, and
- state $q_B$ is next
Alan Turing¶
- “On Computable Numbers, With an Application to the Entscheidungsproblem” (1936)
- Latter due to Hilbert and Ackermann in 1928
- Mechanically decide whether a formula is provable from axioms
- Turing called them automatic machines or a-machines
- All done on paper (!) to formalize computability
Nondeterministic Turing Machine¶
$\LARGE{M = (Q, \Sigma, \iota, F, \delta)}$
where
$Q$ is a finite set of states
$\Sigma$ is the finite tape alphabet
$\iota\in Q$ is the initial state
$F\subseteq Q$ is the set of accepting states
$\delta\subseteq(Q\times\Sigma)\times(Q\times\Sigma\times\{L,N,R\})$ is the transition relation
What is nondeterminism?¶
- Faced with any choice, the nondeterministic machine guesses correctly
- Erik Demaine: “How do you engineer luck?”
- Nevertheless a useful theoretical limit
- Let’s encode the rules …
Winning the Game¶
- Nondeterministic $M$ accepts $\mathcal{L}$ in polynomial time $T = Q(n)$
- Then $M$ scans no tape square beyond $T$
- Given input $w$, construct formula $A(w)$ satisfiable iff $M$ accepts $w$
z3.Not(A(w))holds iff $w\not\in\mathcal{L}$
Exactly one tape square scanned each step¶
Let $S_{s,t}$ be true iff square $s$ is scanned at time $t$. Then
$$B_t = (S_{1,t}\lor S_{2,t}\lor\cdots\lor S_{2,T})\land\left[\bigwedge_{1\leq i<j\leq T} (\lnot S_{i,t}\lor \lnot S_{j,t}) \right]$$
$$B = \bigwedge_{1\leq i\leq T} B_i$$
$$\lvert B\rvert = \mathcal{O}(T^3)$$
Exactly one symbol in each square¶
Let $P_{s,t}^i$ be true iff tape square $s$ at step $t$ holds $\sigma_i$. Then
$$C_{s,t} = \bigvee_i P_{s,t}^i\land\left[\bigwedge_{1\leq j < k} (\lnot P_{s,t}^j\lor\lnot P_{s,t}^k)\right]$$
$$C = \bigwedge_{1\leq s,t\leq T} C_{s,t}$$
$$\lvert C\rvert = \mathcal{O}(T^2)$$
Exactly one state at each step¶
Let $Q^i_t$ by true iff $M$ at step $t$ is in state $q_i$. Then
$$D_t = (Q_t^0\lor Q_t^1\lor\cdots)\land\left[\bigwedge_{1\leq i<j} (\lnot Q_t^i\lor\lnot Q_t^j)\right]$$
$$D = \bigwedge_{1\leq i\leq T} D_i$$
$$\lvert D\rvert = \mathcal{O}(T)$$
M is properly initialized¶
$$E = Q_1^0\land S_{1,1}\land P_{1,1}^{i_1}\land\cdots\land P_{n,1}^{i_n}\land P_{n+1,1}^1\land P_{n+2}^2\land\cdots$$where $w = \sigma_i\ldots\sigma_n$, $q_0$ is the start state, and $\sigma_1$ is the blank symbol.
Recall:
- $P^i_{s,t}$ iff tape square $s$ at step $t$ holds $\sigma_i$
- $Q^i_t$ iff at step $t$ the machine is in state $q_i$
- $S_{s,t}$ iff at time $t$ the machine scans square number $s$
$$\lvert E\rvert = \mathcal{O}(T)$$
M adheres to transition relation¶
Let $F$, $G$, and $H$ constrain $P$, $Q$, and $S$ at each step $t$. For example
$$G_{i,j}^t = \bigwedge_{s=1}^{T} (\lnot Q_t^i\lor \lnot S_{s,t}\lor\lnot P_{s,t}^j\lor Q_{t+1}^k)$$requires state $q_i$ scanning $\sigma_j$ to transition to appropriate $q_k$.
- $\lvert F\rvert = \mathcal{O}(T^2)$ — tape updates
- $\lvert G\rvert = \mathcal{O}(T^2)$ — legal state transitions
- $\lvert H\rvert = \mathcal{O}(T^3)$ — scan single square per step
Reach an accept state¶
$$I = \bigvee_t (Q_t^{f_1}\lor\cdots\lor Q_t^{f_n})$$where accept states are $F = {q_{f_1},\ldots,q_{f_n}}$.
$$\lvert I\rvert = \mathcal{O}(T)$$
Another Logical Formula¶
$$A(w) = B\land C\land D\land E\land F\land G\land H\land I$$- Declares successful computation history of polynomial size $Q(T)$
- Enormous formula
- … but polynomially bounded!
- So what have we accomplished?
“The Complexity of Theorem-Proving Procedures”¶
Stephen A. Cook, Image credit: Jiří JaníčekPokud, CC BY-SA 3.0
- 1971 paper showed any problem in NP at most polynomially harder than SAT
- Established SAT as the first problem in NP-complete
- We just walked through the proof
$$\forall p\in\mathbf{NP}, c\in\mathbf{NP}\mathrm{-complete}, p \leq_P c$$
In [31]:
plot_complexity_venn()
In Conclusion¶
- Attacking the problem backwards motivates why SAT solvers matter
- Add this powerful technique to your bag of tricks
- P versus NP is one of the most important open problems in science