$ English peg Solitaire $ 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: $ 0: 1->3 10: 7->9 20: 10->24 30: 14->16 40: 18->6 50: 23->9 60:25->33 70:30->28 $ 1: 1->9 11: 7->21 21: 10->8 31: 15->17 41: 18->20 51: 23->25 61:25->23 71:31->23 $ 2: 2->10 12: 8->10 22: 11->3 32: 16->4 42: 18->30 52: 23->31 62:26->23 72:31->33 $ 3: 3->1 13: 8->22 23: 11->13 33: 16->18 43: 18->16 53: 23->21 63:26->24 73:32->24 $ 4: 3->11 14: 9->1 24: 11->25 34: 16->28 44: 19->17 54: 24->10 64:27->13 74:33->25 $ 5: 4->6 15: 9->11 25: 11->9 35: 16->14 45: 20->18 55: 24->26 65:27->25 75:33->31 $ 6: 4->16 16: 9->23 26: 12->26 36: 17->5 46: 21->23 56: 24->32 66:28->16 $ 7: 5->17 17: 9->7 27: 12->10 37: 17->19 47: 21->7 57: 24->22 67:28->30 $ 8: 6->4 18: 10->2 28: 13->27 38: 17->29 48: 22->8 58: 25->11 68:29->17 $ 9: 6->18 19: 10->12 29: 13->11 39: 17->15 49: 22->24 59: 25->27 69:30->18 $ ---------------------------------------------------------------- $ legal transitions forall step : int(0..noSteps-1) . forall f1,f2 : FIELDS . $ if there exists a legal transition from f1 to f2 ((transitionNumber[f1,f2] != 0) /\ (f1 != f2)) => $ and we make that transition, the following holds.. ( (moves[step] = transitionNumber[f1,f2]) <=> $ effect and precondition ( (bState[step, f1] > bState[step+1,f1]) /\ (bState[step,transitionStep[transitionNumber[f1,f2],2]] > bState[step+1, transitionStep[transitionNumber[f1,f2],2]]) /\ (bState[step, f2] < bState[step+1, f2]) /\ $ frame axiom forall field : FIELDS . ( (field != f1) /\ (field != transitionStep[transitionNumber[f1,f2],2]) /\ (field != f2) ) => (bState[step,field] = bState[step+1,field]) ) )