Satisfiability and Peg Solitaire

 This page contains information on using SAT solvers such as zChaff to handle simple puzzles such as peg solitaire.

Description of peg solitaire

 Peg solitaire describes a general class of peg-jumping games in which a player is initially presented with a board containing holes and wooden pegs filling a subset of these holes. For any given move, a player must select one of the pegs on the board which has an adjacent peg and an empty hole following that adjacent peg. The original peg is moved to the empty hole and the adjacent "jumped" peg is removed from the board. The game ends when no more legal "jumps" may be made. The object of the game is to remove all pegs from the board except one. Below is an example of a board configuration and move transition: 
		        O                       #         
		       / \                     / \        
		      # - O                   O - O          # = peg
		     / \ / \                 / \ / \         O = empty hole
		    # - # - #     ---->     O - # - #
		   / \ / \ / \             / \ / \ / \
		  O - # - # - O           O - # - # - O
		 / \ / \ / \ / \         / \ / \ / \ / \
		O - O - O - O - O       O - O - O - O - O

	Figure 1: Sample board configuration and move.
Typically in the initial board configuration, all holes have pegs except one; ideally, the one initially empty hole should be the only peg with a hole in the final state.

Back to the top.

Turning peg solitaire into a boolean expression

 The general idea behind encoding peg solitaire as a boolean expression is to represent each possible move or transition in the game as a conjunction of several boolean conditions that must be met in order for the move to be possible. Consider the following board numbering scheme, for instance: 
		        0
		       / \
		      1 - 2
		     / \ / \
		    3 - 4 - 5
		   / \ / \ / \
		  6 - 7 - 8 - 9
		 / \ / \ / \ / \
		10- 11- 12- 13- 14

	Figure 2: Board numbering scheme.
Let p0...p14 be truth values representing the state of the board before a move is made, and let q0...q14 be the truth values representing the state of the board after the move is made. pi is true if and only if a peg is found at location i before the move is made; likewise, qj is true if and only if a peg is found at location j after the move has been made. For example, if we consider the move from Figure 1, the truth values for p0...p14 and q0...q14 are:

i 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14
pi false true true false true true false true true false false false false false false
qi true false false false true true false true true false false false false false false 
	Figure 3: Move transition boolean values.

Now, let us denote a move by the ordered triple (i, j, k) designating that peg i jumps over peg j and ends up at hole k. For instance, in the example above, the move performed was (3, 1, 0). Given a pair of board configurations p0...p14 and q0...q14 and a move (i, j, k), we can test to see if the move given applied to board p results in board q. To do this, we must simply check that pegs initially existing at positions i and j in board p no longer exist in board q and that hole k which was originally empty in p is now filled in q. We must also check that all other states besides holes i, j, and k are not affected. The following boolean expression does the trick for the move (3, 1, 0): 
		valid(p, q, (3, 1, 0)) =    (p3 & ~q3) &    (p1 & ~q1) &    (~p0 & q0) &
		                           (p2 <-> q2) &   (p4 <-> q4) &   (p5 <-> q5) &
		                           (p6 <-> q6) &   (p7 <-> q7) &   (p8 <-> q8) &
		                           (p9 <-> q9) & (p10 <-> q10) & (p11 <-> q11) &
		                         (p12 <-> q12) & (p13 <-> q13) & (p14 <-> q14)

	Figure 4: Boolean expression for checking move transition.
The above expression evaluates to true only when p0...p14 and q0...q14 represent board states such that performing the move (3, 1, 0) turns board p into board q. If any of the given conditions evaluates to a false, then the whole expression evaluates to a false. This expression, however, can be generalized to check for all valid moves by constructing expressions for each of the 36 possible different moves at any given board position and taking the OR of their evaluations. In other words, the generalized expression would involve only the variables p0...p14 and q0...q14 and would return true if and only if a legal move turns board p into board q. For convenience, let us denote this generalized expression as legal(p, q): 
		legal(p, q) = valid(p, q, ( 0,  1,  3)) | valid(p, q, ( 3,  1,  0)) |
		              valid(p, q, ( 0,  2,  5)) | valid(p, q, ( 5,  2,  0)) |
		              valid(p, q, ( 1,  3,  6)) | valid(p, q, ( 6,  3,  1)) |
		              valid(p, q, ( 1,  4,  8)) | valid(p, q, ( 8,  4,  1)) |
		              valid(p, q, ( 2,  4,  7)) | valid(p, q, ( 7,  4,  2)) |
		              valid(p, q, ( 2,  5,  9)) | valid(p, q, ( 9,  5,  2)) |
		              valid(p, q, ( 3,  4,  5)) | valid(p, q, ( 5,  4,  3)) |
		              valid(p, q, ( 3,  6, 10)) | valid(p, q, (10,  6,  3)) |
		              valid(p, q, ( 3,  7, 12)) | valid(p, q, (12,  7,  3)) |
		              valid(p, q, ( 4,  7, 11)) | valid(p, q, (11,  7,  4)) |
		              valid(p, q, ( 4,  8, 13)) | valid(p, q, (13,  8,  4)) |
		              valid(p, q, ( 5,  8, 12)) | valid(p, q, (12,  8,  5)) |
		              valid(p, q, ( 5,  9, 14)) | valid(p, q, (14,  9,  5)) |
		              valid(p, q, ( 6,  7,  8)) | valid(p, q, ( 8,  7,  6)) |
		              valid(p, q, ( 7,  8,  9)) | valid(p, q, ( 9,  8,  7)) |
		              valid(p, q, (10, 11, 12)) | valid(p, q, (12, 11, 10)) |
		              valid(p, q, (11, 12, 13)) | valid(p, q, (13, 12, 11)) |
		              valid(p, q, (12, 13, 14)) | valid(p, q, (14, 13, 12))

	Figure 5: Generalized boolean expression for checking move validity.
Formation of a boolean expression that solves the game of peg solitaire then follows easily from the above. Note that in a game of peg solitaire where originally 15 - 1 = 14 pegs originally occupy the board, only 1 is left at the end, meaning that 13 moves must be made or 14 board states exist at different points in time. Let bi represent the board configuration after i moves have been made where (bi)j is the state of peg j on board i. In order to check if a set of boolean values for b solves the game of peg solitaire, we simply check to make sure that the transition between every board configuration in b is legal as follows: 
		won(b) = legal( b0,  b1) & legal( b1,  b2) & legal( b2,  b3) & legal( b3,  b4) &
		         legal( b4,  b5) & legal( b5,  b6) & legal( b6,  b7) & legal( b7,  b8) &
		         legal( b8,  b9) & legal( b9, b10) & legal(b10, b11) & legal(b11, b12) &
		         legal(b12, b13)

	Figure 6: Boolean expression for checking solitaire game validity.
Thus, solving the game of peg solitaire has been reduced to finding a set of boolean values for b such won(b) evaluates to true.

Back to the top.

Encoding peg solitaire in Conjunctive Normal Form (CNF)

 Many programs already exist to accomplish the task described above: finding a set of boolean values such that an expression evaluates to true. These satisfiability programs, also known as SAT solvers, use highly specialized and optimized methods for satisfiability computation. One such program is the freeware SAT solver, zChaff. The source code for zChaff is readily available for academic purposes from the website for the Boolean Satisfiability Research Group at Princeton. In order to use zChaff to solve the peg solitaire problem, the peg solitaire boolean expression must be expressed in conjunctive normal form (CNF). A boolean expression in CNF is one which takes the form P1 & P2 & ... & Pn where each Pi is of the form p1 | p2 | ... | pn. The main ideas behind reducing the given expression to conjunctive normal form are as follows:
  1. In order to save on the computation involved, notice that in general, if (i, j, k) is a possible move for some board configuration, then (k, j, i) is also a possible move for some other board configuration. In either case, the requirements that all other pieces on the board remain the same are identical. Thus, those may be factored out so that the remaining computation only involves calculating the "no change" parameters for the board once.
  2. Simplification of the biconditionals used for "no change" predicates used the transformation: 
    		(P <-> Q) <=> (P -> Q) & (Q -> P)
		          <=> (~P | Q) & (P | ~Q).

	Figure 7: Transformation of P <-> Q.
  3. At this point, to check that a move is valid requires ANDing the result of several expression containing only NOTs and ORs. However, we must now be able to allow for the selection of one and only one valid move among those available. Here, we introduce the following technique for encoding ORs of large expession blocks. Suppose we wish to encode the following expression in CNF: 
    		((P1)1 & (P1)2 & ... & (P1)N1) |
		((P2)1 & (P2)2 & ... & (P2)N2) |
		...
		((PM)1 & (PM)2 & ... & (PM)N3)

		where (Pi)j are expressions of the form p1 | p2 | ... | pk.

	Figure 8: Expression to be encoded in CNF.
    This may be encoded in a fairly straightforward manner by introducing "selection variables" S1, S2... such that each expression that is ORed maps directly to some particular combination of selection values. Given M expressions to be ORed, at least log2 M selection variables are needed. Any combination of selection variables not assigned to an expression should be mapped to false to ensure that the CNF expression does not produce any board configurations using them. For example, 
    		Encoding the expression

		(P1 & P2 & P3) | (Q1 & Q2) | (R1 & R2 & R3 & R4)

		gives

		( S1 |  S2 | P1) &	<-- If (!S1 & !S2) then all rules for P must be satisfied.
		( S1 |  S2 | P2) &
		( S1 |  S2 | P3) &

		( S1 | ~S2 | Q1) &	<-- If (!S1 & S2) then all rules for Q must be satisfied.
		( S1 | ~S2 | Q2) &

		(~S1 |  S2 | R1) &	<-- If (S1 & !S2) then all rules for R must be satisfied.
		(~S1 |  S2 | R2) &
		(~S1 |  S2 | R3) &
		(~S1 |  S2 | R4) &

		(~S1 | ~S2)		<-- Any possibilities with (S1 & S2) are discarded.

	Figure 9: Log2 encoding of ORs in CNF.
  4. In the case of triangle peg solitaire, there are 36 possible moves possible in a generic board configuration in which the location of the pegs has not yet been specified. Each pair of possible moves as noted earlier requires only one validity check for the "no change" predicates. Consequently, there are 18 validity conditions that must be checked and ORed together to determine if a legal move exists for the given board configuration, so 5 selection variables are needed to pick a valid rule. Note, however, that many of these rules (32 - 18 = 14) are left unused and must therefore be discarded. We may save on computation by factoring out commonalities between these expressions. For instance, 
    		The null expressions are:

		(~S1 |  S2 |  S3 | ~S4 |  S5) &
		(~S1 |  S2 |  S3 | ~S4 | ~S5) &
		(~S1 |  S2 | ~S3 |  S4 |  S5) &
		(~S1 |  S2 | ~S3 |  S4 | ~S5) &
		(~S1 |  S2 | ~S3 | ~S4 |  S5) &
		(~S1 |  S2 | ~S3 | ~S4 | ~S5) &
		(~S1 | ~S2 |  S3 |  S4 |  S5) &
		(~S1 | ~S2 |  S3 |  S4 | ~S5) &
		(~S1 | ~S2 |  S3 | ~S4 |  S5) &
		(~S1 | ~S2 |  S3 | ~S4 | ~S5) &
		(~S1 | ~S2 | ~S3 |  S4 |  S5) &
		(~S1 | ~S2 | ~S3 |  S4 | ~S5) &
		(~S1 | ~S2 | ~S3 | ~S4 |  S5) &
		(~S1 | ~S2 | ~S3 | ~S4 | ~S5)

		which may be factored to give:

		(~S1 |  S2 |  S3 | ~S4) &
		(~S1 |  S2 | ~S3) &
		(~S1 | ~S2)

	Figure 10: Factoring out common expressions.
The above describes the basic ideas for conversion of the peg solitaire satisfiability expression to CNF. Putting this CNF expression in a form readable by zChaff is a technical matter. zChaff accepts files given in DIMACS cnf format which is described at the SATLIB satisfiability page.

Back to the top.

An alternative rule-based encoding scheme

 The earlier method for encoding peg solitaire is not, of course, the only method possible. An alternative rule-based encoding was also tried and yielded some encouraging results. Board representation is identical as with the earlier approach, but the difference comes in computing valid move transitions. In the earlier scheme, moves were represented as changes in a board state in which some holes were filled, others were emptied, and the rest did not change. The inefficiency of such a method is that a solver must individually check the transition states of each hole for each possible move in a certain board state. To reduce redundancy, the rule-based mechanism works as follows:
  1. For any given board state, a rule is created for each possible transition, in which the rule checks to make sure that the desired move is valid given the current board configuration and that any affected squares are changed in the goal board configuration.
  2. All board positions are checked to make sure that squares in the goal board configuration are identical to those before the move transition except those affected by the current rule.
  3. Rules are checked to make sure that exactly one rule is active for any board transition.
The first part of this process, the encoding of the rules, may be further compressed by combining the rules for move transitions that involve the same block of squares. This may be done as follows for the moves (0, 1, 3) and (3, 1, 0): 
		~rule013 | p1		<-- This pair to make sure that peg 1 exists
		~rule013 | ~q1		    before the move and is removed after the
					    transition.

		~rule013 | ~p3 | ~p0	<-- This pair ensures that either peg 0 or
		~rule013 | p3 | p0	    peg 3 is present before the move (so as
					    to make sure that the jumping peg has a
					    hole to jump into).

		~rule013 | ~p3 | ~q3	<-- These four rules ensure that the states
		~rule013 | p3 | q3	    for peg 0 and peg 3 have changed, regardless
		~rule013 | ~p1 | ~q1	    whether peg 0 jumps over peg 1 to get to
		~rule013 | p1 | q1	    hole 3 or whether peg 3 jumps over peg 1 to
					    get to hole 0.

	Figure 11: Rule set for the moves (0, 1, 3) and (3, 1, 0).
As seen, the rule is simple in construction. The use of ~rule013 at the beginning of each requirement in the rule set ensures that the rule is obeyed unless it is not active. Checking of board transition states for any given state may then be done as follows: 
		~p0  |  q0  | rule013 | rule025
		 p0  | ~q0  | rule013 | rule025
		~p1  |  q1  | rule013 | rule136 | rule148
		 p1  | ~q1  | rule013 | rule136 | rule148
		~p2  |  q2  | rule025 | rule247 | rule259
		 p2  | ~q2  | rule025 | rule247 | rule259
		~p3  |  q3  | rule013 | rule136 | rule345 | rule3610 | rule3712
		 p3  | ~q3  | rule013 | rule136 | rule345 | rule3610 | rule3712
		~p4  |  q4  | rule148 | rule247 | rule345 | rule4711 | rule4813
		 p4  | ~q4  | rule148 | rule247 | rule345 | rule4711 | rule4813
		~p5  |  q5  | rule025 | rule259 | rule345 | rule5812 | rule5914
		 p5  | ~q5  | rule025 | rule259 | rule345 | rule5812 | rule5914
		~p6  |  q6  | rule136 | rule3610 | rule678
		 p6  | ~q6  | rule136 | rule3610 | rule678
		~p7  |  q7  | rule247 | rule3712 | rule4711 | rule678 | rule789
		 p7  | ~q7  | rule247 | rule3712 | rule4711 | rule678 | rule789
		~p8  |  q8  | rule148 | rule4813 | rule5812 | rule678 | rule789
		 p8  | ~q8  | rule148 | rule4813 | rule5812 | rule678 | rule789
		~p9  |  q9  | rule259 | rule789 | rule5914
		 p9  | ~q9  | rule259 | rule789 | rule5914
		~p10 |  q10 | rule3610 | rule101112
		 p10 | ~q10 | rule3610 | rule101112
		~p11 |  q11 | rule4711 | rule101112 | rule111213
		 p11 | ~q11 | rule4711 | rule101112 | rule111213
		~p12 |  q12 | rule3712 | rule5812 | rule101112 | rule111213 | rule121314
		 p12 | ~q12 | rule3712 | rule5812 | rule101112 | rule111213 | rule121314
		~p13 |  q13 | rule4813 | rule111213 | rule121314
		 p13 | ~q13 | rule4813 | rule111213 | rule121314
		~p14 |  q14 | rule5914 | rule121314
		 p14 | ~q14 | rule5914 | rule121314

	Figure 12: Rule-based board transition.
Finally, the rules may be checked to ensure that only one is active at any time. This may be done as follows: 

		rule013 | rule025 | rule136 |  ...	<-- Ensures that at least one rule
							    is selected.

		~rule013 | ~rule025			<-- Ensures that no two rules are
		~rule013 | ~rule136			    simultaneously selected.
		~rule013 | ~rule148
			...
		~rule025 | ~rule136
		~rule025 | ~rule148
			...
	
	Figure 13: Rule selection.
As seen, this encoding is much more straightforward and easier to put in the required CNF format.

Back to the top.

Results and relevant files

 The resulting run-times given the various encodings were as follows:

Puzzle Type Board-change Encoding Rule-based Encoding
Triangle peg solitaire 1.55 s 0.06 s
Hi-Q: Cross 0.09 s 0 s
Hi-Q: Plus 0.13 s 0.01 s
Hi-Q: Fireplace 16.34 s 0.03 s
Hi-Q: Up-Arrow 5108.76 s 95.2 s
Hi-Q: Diamond 353.31 s 0.35 s
Hi-Q: Pyramid 0.73 s 0.26 s
Hi-Q: Solitaire 4408.21 s > 172800 s

To access files related to the board-change encoding scheme, click here.
To access files related to the rule-based encoding scheme, click here.

In all cases except the solitaire puzzle, the rule-based encoding far outperforms the board-change method. For the present, no specific conclusions will be made, though the more natural encoding does indeed seem to have an edge. The reasons for the performance hit when faced with the big solitaire puzzle are as of yet unknown. Stay tuned...

Back to the top.
Comments to Chuong Do (chuong.do@stanford.edu)