- General Information and Basic Techniques
- Results and Discussion

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.

0 / \ 1 - 2 / \ / \ 3 - 4 - 5 / \ / \ / \ 6 - 7 - 8 - 9 / \ / \ / \ / \ 10- 11- 12- 13- 14 Figure 2: Board numbering scheme.Let p

i | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 |

p_{i} |
false | true | true | false | true | true | false | true | true | false | false | false | false | false | false |

q_{i} |
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 p

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 p

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 b

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.

- 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.
- 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.

- 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" S_{1}, S_{2}... such that each expression that is ORed maps directly to some particular combination of selection values. Given M expressions to be ORed, at least log_{2}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.

- 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.

Back to the top.

- 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.
- 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.
- Rules are checked to make sure that exactly one rule is active for any board transition.

~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.

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.