$ English peg Solitaire $ following the CP model in $ Modelling and Solving English Peg Solitaire, C. Jefferson, A. Miguel, I. Miguel, A. Tarim. $ http://www.dcs.st-and.ac.uk/~ianm/docs/CAORPreprint.pdf $ $ english board version: $ $ 0 0 * * * 0 0 $ 0 0 * * * 0 0 $ * * * * * * * $ * * * * * * * $ * * * * * * * $ 0 0 * * * 0 0 $ 0 0 * * * 0 0 $ 00000 1 2 3 00000 $ 00000 4 5 6 00000 $ 7 8 9 10 11 12 13 $ 14 15 16 17 18 19 20 $ 21 22 23 24 25 26 27 $ 00000 28 29 30 00000 $ 00000 31 32 33 00000 $ modelled by Andrea Rendl $ $ ---------------------------------------------------------------- language ESSENCE' 1.b.a $ gives the transitionNumber: transitionNumber[i,j] returns the $ transition number when jumping from field i to field j $ (if transition does not exist -> 0) letting transitionNumber : matrix indexed by [int(1..33),int(1..33)] of int(0..76) be $ 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 [ [0, 0, 1, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $1 [0, 0, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $2 [4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $3 [0, 0, 0, 0, 0, 6, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $4 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $5 [0, 0, 0, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,10, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $6 [0, 0, 0, 0, 0, 0, 0, 0, 12,0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,11, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $7 [0, 0, 0, 0, 0, 0, 0, 0, 0,13, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 14,0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $8 [18,0, 0, 0, 0, 0,15, 0, 0, 0, 17,0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,16, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $9 [0,19, 0, 0, 0, 0, 0,22, 0, 0, 0,20, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,21, 0, 0, 0, 0, 0, 0, 0, 0, 0], $10 [0, 0,23, 0, 0, 0, 0, 0,26, 0, 0, 0,24, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,25, 0, 0, 0, 0, 0, 0, 0, 0], $11 [0, 0, 0, 0, 0, 0, 0, 0, 0,27, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,28, 0, 0, 0, 0, 0, 0, 0], $12 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0,30, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,29, 0, 0, 0, 0, 0, 0], $13 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,31, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $14 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,32, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $15 [0, 0, 0,34, 0, 0, 0, 0, 0, 0, 0, 0, 0,33, 0, 0, 0,36, 0, 0, 0, 0, 0, 0, 0, 0, 0,35, 0, 0, 0, 0, 0], $16 [0, 0, 0, 0,38, 0, 0, 0, 0, 0, 0, 0, 0, 0,37, 0, 0, 0,40, 0, 0, 0, 0, 0, 0, 0, 0, 0,39, 0, 0, 0, 0], $17 [0, 0, 0, 0, 0,42, 0, 0, 0, 0, 0, 0, 0, 0, 0,41, 0, 0, 0,44, 0, 0, 0, 0, 0, 0, 0, 0, 0,43, 0, 0, 0], $18 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,45, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $19 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,46, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $20 [0, 0, 0, 0, 0, 0,47, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,48, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $21 [0, 0, 0, 0, 0, 0, 0,50, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,49, 0, 0, 0, 0, 0, 0, 0, 0, 0], $22 [0, 0, 0, 0, 0, 0, 0, 0,52, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,51, 0, 0, 0,54, 0, 0, 0, 0, 0,53, 0, 0], $23 [0, 0, 0, 0, 0, 0, 0, 0, 0,56, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,55, 0, 0, 0,57, 0, 0, 0, 0, 0,58, 0], $24 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0,60, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,59, 0, 0, 0,62, 0, 0, 0, 0, 0,61], $25 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,64, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,63, 0, 0, 0, 0, 0, 0, 0, 0, 0], $26 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,65, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,66, 0, 0, 0, 0, 0, 0, 0, 0], $27 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,68, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,67, 0, 0, 0], $28 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,69, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], $29 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,71, 0, 0, 0, 0, 0, 0, 0, 0, 0,70, 0, 0, 0, 0, 0], $30 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,73, 0, 0, 0, 0, 0, 0, 0, 0, 0,72], $31 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,74, 0, 0, 0, 0, 0, 0, 0, 0, 0], $32 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,76, 0, 0, 0, 0, 0,75, 0, 0] $33 ] $ transitionStep[t, i] returns the ith field (of three) that is $ altered during translation step number t letting transitionStep : matrix indexed by [int(1..76),int(1..3)] of int(1..33) be [ [ 1,2,3], [1,4,9], [2,5,10], [3,2,1], [3,6,11],[4,5,6], [4,9,16], [5,10,17], [6,5,4], [6,11,18], [7,14,21], [ 7,8,9], [8,9,10], [8,15,22],[9,8,7], [9,16,23], [9,10,11], [9,4,1], [10,5,2], [10,11,12], [10,17,24], [10,9,8], [11,6,3], [11,12,13],[11,18,25], [11,10,9], [12,11,10],[12,19,26],[13,20,27], [13,12,11], [14,15,16], [15,16,17], [16,15,14], [16,9,4], [16,23,28], [16,17,18],[17,16,15], [17,10,5],[17,24,29], [17,18,19], [18,17,16], [18,11,6], [18,25,30], [18,19,20], [19,18,17], [20,19,18], [21,14,7], [21,22,23], [22,23,24], [22,15,8], [23,22,21], [23,16,9],[23,28,31], [23,24,25],[24,23,22],[24,17,10],[24,25,26],[24,29,32], [25,24,23],[25,18,11], [25,30,33], [25,26,27], [26,25,24],[26,19,12],[27,20,13],[27,26,25],[28,29,30],[28,23,16],[29,24,17],[30,29,28], [30,25,18], [31,32,33], [31,28,23], [32,29,24], [33,32,31] ,[33,30,25] ] $ noSteps-1 -> we start counting with 0 given noSteps : int $ 231 given startField : int(1..33) letting noFields be 33 letting STEPS be domain int(0..noSteps) letting FIELDS be domain int(1..33) $ ---------------------------------------------------------------- $ we can solve the problem in 31 steps by making one out of 76 transitions find moves: matrix indexed by [int(0..noSteps-1)] of int(1..76) $ bState[t,f] is set to true if for step t field f is occupied find bState: matrix indexed by [STEPS, FIELDS] of bool $ ---------------------------------------------------------------- such that $ ---------------------------------------------------------------- $ initial state: all fields are occupied but the one in the centre forall i : FIELDS . (i != startField) => (bState[0,i] = true), bState[0,startField] = false, $ ---------------------------------------------------------------- $ goal state : only one field is occupied forall step : STEPS . noFields-step-1 = (sum i : FIELDS . bState[step,i]), $= noFields-step-1, $30, $1, $ ---------------------------------------------------------------- $ Allowed transitions: $ 1: 1->3 11: 7->9 21: 10->24 31: 14->16 41: 18->6 51: 23->9 61:25->33 71:30->28 $ 2: 1->9 12: 7->21 22: 10->8 32: 15->17 42: 18->20 52: 23->25 62:25->23 72:31->23 $ 3: 2->10 13: 8->10 23: 11->3 33: 16->4 43: 18->30 53: 23->31 63:26->12 73:31->33 $ 4: 3->1 14: 8->22 24: 11->13 34: 16->18 44: 18->16 54: 23->21 64:26->24 74:32->24 $ 5: 3->11 15: 9->1 25: 11->25 35: 16->28 45: 19->17 55: 24->10 65:27->13 75:33->25 $ 6: 4->6 16: 9->11 26: 11->9 36: 16->14 46: 20->18 56: 24->26 66:27->25 76:33->31 $ 7: 4->16 17: 9->23 27: 12->26 37: 17->5 47: 21->23 57: 24->32 67:28->16 $ 8: 5->17 18: 9->7 28: 12->10 38: 17->19 48: 21->7 58: 24->22 68:28->30 $ 9: 6->4 19: 10->2 29: 13->27 39: 17->29 49: 22->8 59: 25->11 69:29->17 $ 10:6->18 20: 10->12 30: 13->11 40: 17->15 50: 22->24 60: 25->27 70:30->18 $ ---------------------------------------------------------------- $ legal transitions forall step : int(0..noSteps-1) . forall f : FIELDS . (bState[step, f] = bState[step+1,f]) <=> (forall f1 : FIELDS . $ (f != f1) => ( (moves[step] != transitionNumber[f,f1]) /\ (moves[step] != transitionNumber[f1,f]) /\ forall f2 : FIELDS . $ (f1 != f2) => ((( transitionNumber[f1,f2] != 0) => ((f = transitionStep[transitionNumber[f1,f2],2]) => (moves[step] != transitionNumber[f1,f2]) ) ) /\ (( transitionNumber[f2,f1] != 0) => ( (f = transitionStep[transitionNumber[f2,f1],2]) => (moves[step] != transitionNumber[f2,f1]) ) )) ) ), forall step : int(0..noSteps-1) . forall f : FIELDS . $ 0 -> 1 (bState[step,f] < bState[step+1,f]) <=> exists f1 : FIELDS . (transitionNumber[f1,f] != 0) /\ (moves[step] = transitionNumber[f1,f]), forall step : int(0..noSteps-1) . forall f : FIELDS . $ 1 peg -> 0 pegs (bState[step,f] > bState[step+1,f]) <=> (exists f1 : FIELDS . $ middle peg (exists f2 : FIELDS . $ (f1 != f2) /\ (f != f2) /\ (moves[step] = transitionNumber[f1,f2]) /\ ( transitionNumber[f1,f2] != 0) /\ (f = transitionStep[transitionNumber[f1,f2],2]) $/\ $ (f1 != f2) /\ (f != f2) ) \/ $ start peg ( $(f != f) /\ ((transitionNumber[f,f1] != 0) /\ (moves[step] = transitionNumber[f,f1])) ) )