$ Black Hole Solitaire $ $ starting from 17 stacks of 3 cards and the spades ace in the middle $ (the black hole), cards are put on top of the black hole. $ It will accept a card if its rank is one greater or one less than $ the rank of the card currently on top of it. The objective is to $ remove all the cards from the stacks onto the black hole. $ $ modelled by Andrea Rendl $ after the model in 'Search in the Patience Game 'Black Hole'.' $ I. Gent, C. Jefferson, I. Lynce, I. Miguel, P. Nightingale, B. Smith and A. Tarim language ESSENCE' 1.b.a letting noSteps be 51 letting STEPS be domain int(0..noSteps) letting STEPS1 be domain int(1..noSteps) letting SPADES be 0 letting HEARTS be 1 letting CLUBS be 2 letting DIAMONDS be 3 letting CARDS_NO_ACE be domain int(1..51) letting SUITS be domain int(0..3) letting CARDS be domain int(0..51) given initialStacks : matrix indexed by [CARDS] of CARDS_NO_ACE $ the sequence of ranks for each step find blackHole : matrix indexed by [STEPS] of CARDS $ the cards and their position in the sequence find cardSequence : matrix indexed by [CARDS] of STEPS $ height 3: topmost card $ height 2: middle card $ height 1: lowest card $find height : matrix indexed by [CARDS_NO_ACE] of int(1..3) such that $ initial state: the spades ace in in the middle blackHole[0] = 0, cardSequence[0] = 0, alldifferent(cardSequence), alldifferent(blackHole), $ allowed pairs $forall step : STEPS1 . $ exists suit : SUITS . $ ( (blackHole[step] = (blackHole[step-1]%13)-1 + 13*suit) \/ $ (blackHole[step] = (blackHole[step-1]%13)+1 + 13*suit) $ ), forall step : STEPS1 . table([blackHole[step-1],blackHole[step]], [ [0,1], [0,14], [0,27], [0,40], [0,-1], [0,12], [0,25], [0,38], [1,2], [1,15], [1,28], [1,41], [1,0], [1,13], [1,26], [1,39], [2,3], [2,16], [2,29], [2,42], [2,1], [2,14], [2,27], [2,40], [3,4], [3,17], [3,30], [3,43], [3,2], [3,15], [3,28], [3,41], [4,5], [4,18], [4,31], [4,44], [4,3], [4,16], [4,29], [4,42], [5,6], [5,19], [5,32], [5,45], [5,4], [5,17], [5,30], [5,43], [6,7], [6,20], [6,33], [6,46], [6,5], [6,18], [6,31], [6,44], [7,8], [7,21], [7,34], [7,47], [7,6], [7,19], [7,32], [7,45], [8,9], [8,22], [8,35], [8,48], [8,7], [8,20], [8,33], [8,46], [9,10], [9,23], [9,36], [9,49], [9,8], [9,21], [9,34], [9,47], [10,11], [10,24], [10,37], [10,50], [10,9], [10,22], [10,35], [10,48], [11,12], [11,25], [11,38], [11,51], [11,10], [11,23], [11,36], [11,49], [12,13], [12,26], [12,39], [12,0], [12,11], [12,24], [12,37], [12,50], [13,14], [13,27], [13,40], [13,1], [13,12], [13,25], [13,38], [13,51], [14,15], [14,28], [14,41], [14,2], [14,13], [14,26], [14,39], [14,0], [15,16], [15,29], [15,42], [15,3], [15,14], [15,27], [15,40], [15,1], [16,17], [16,30], [16,43], [16,4], [16,15], [16,28], [16,41], [16,2], [17,18], [17,31], [17,44], [17,5], [17,16], [17,29], [17,42], [17,3], [18,19], [18,32], [18,45], [18,6], [18,17], [18,30], [18,43], [18,4], [19,20], [19,33], [19,46], [19,7], [19,18], [19,31], [19,44], [19,5], [20,21], [20,34], [20,47], [20,8], [20,19], [20,32], [20,45], [20,6], [21,22], [21,35], [21,48], [21,9], [21,20], [21,33], [21,46], [21,7], [22,23], [22,36], [22,49], [22,10], [22,21], [22,34], [22,47], [22,8], [23,24], [23,37], [23,50], [23,11], [23,22], [23,35], [23,48], [23,9], [24,25], [24,38], [24,51], [24,12], [24,23], [24,36], [24,49], [24,10], [25,26], [25,39], [25,0], [25,13], [25,24], [25,37], [25,50], [25,11], [26,27], [26,40], [26,1], [26,14], [26,25], [26,38], [26,51], [26,12], [27,28], [27,41], [27,2], [27,15], [27,26], [27,39], [27,0], [27,13], [28,29], [28,42], [28,3], [28,16], [28,27], [28,40], [28,1], [28,14], [29,30], [29,43], [29,4], [29,17], [29,28], [29,41], [29,2], [29,15], [30,31], [30,44], [30,5], [30,18], [30,29], [30,42], [30,3], [30,16], [31,32], [31,45], [31,6], [31,19], [31,30], [31,43], [31,4], [31,17], [32,33], [32,46], [32,7], [32,20], [32,31], [32,44], [32,5], [32,18], [33,34], [33,47], [33,8], [33,21], [33,32], [33,45], [33,6], [33,19], [34,35], [34,48], [34,9], [34,22], [34,33], [34,46], [34,7], [34,20], [35,36], [35,49], [35,10], [35,23], [35,34], [35,47], [35,8], [35,21], [36,37], [36,50], [36,11], [36,24], [36,35], [36,48], [36,9], [36,22], [37,38], [37,51], [37,12], [37,25], [37,36], [37,49], [37,10], [37,23], [38,39], [38,0], [38,13], [38,26], [38,37], [38,50], [38,11], [38,24], [39,40], [39,1], [39,14], [39,27], [39,38], [39,51], [39,12], [39,25], [40,41], [40,2], [40,15], [40,28], [40,39], [40,0], [40,13], [40,26], [41,42], [41,3], [41,16], [41,29], [41,40], [41,1], [41,14], [41,27], [42,43], [42,4], [42,17], [42,30], [42,41], [42,2], [42,15], [42,28], [43,44], [43,5], [43,18], [43,31], [43,42], [43,3], [43,16], [43,29], [44,45], [44,6], [44,19], [44,32], [44,43], [44,4], [44,17], [44,30], [45,46], [45,7], [45,20], [45,33], [45,44], [45,5], [45,18], [45,31], [46,47], [46,8], [46,21], [46,34], [46,45], [46,6], [46,19], [46,32], [47,48], [47,9], [47,22], [47,35], [47,46], [47,7], [47,20], [47,33], [48,49], [48,10], [48,23], [48,36], [48,47], [48,8], [48,21], [48,34], [49,50], [49,11], [49,24], [49,37], [49,48], [49,9], [49,22], [49,35], [50,51], [50,12], [50,25], [50,38], [50,49], [50,10], [50,23], [50,36], [51,0], [51,13], [51,26], [51,39], [51,50], [51,11], [51,24], [51,37]] ), $ precedence constraint forall card : int(0..50) . (card % 3 != 2) => (cardSequence[initialStacks[card]] < cardSequence[initialStacks[card+1]]), $ channelling constraint forall step : STEPS . forall card : CARDS . (blackHole[step] = card) <=> (cardSequence[card] = step), $ height constraint $forall stack : int(0..16) . $ forall card : int(0..2) . $ height[initialStacks[stack*3+card]] = (card+1)%4, $ Barbara's constraint or what I interpreted from it $ if we have the choice between 2 cards of the same rank, pick the one with higher height $forall card1,card2 : CARDS_NO_ACE . $ 2 cards of the same rank but different suits $ ((card1 % 13 = card2 % 13) /\ (card1 != card2)) => $ the card that is on top of a pile should be picked first $ ((height[card1] > height[card2]) => (cardSequence[card1] > cardSequence[card2])), $ conditional symmetry breaking $ if two cards of the same rank are on the bottom of a stack then take the smaller one $ CASE A of Barbara's model forall stack1, stack2 : int(0..16) . ( (stack1 < stack2) /\ $ the 3rd cards have the same rank (initialStacks[stack1*3+2] % 13 = initialStacks[stack2*3+2] % 13) ) => $ y[cover[c1] < y[c2] => y[c1] < y[c2] ( (cardSequence[initialStacks[stack1*3+1]] < cardSequence[initialStacks[stack2*3+2]] ) => (cardSequence[initialStacks[stack1*3+2]] < cardSequence[initialStacks[stack2*3+2]]) ), $ if two cards of the same rank are on top of a stack $ CASE B of Barbara's model forall stack1, stack2 : int(0..16) . ( (stack1 < stack2) /\ $ the 1st cards have the same rank (initialStacks[stack1*3] % 13 = initialStacks[stack2*3] % 13) ) => $ y[c1] < y[coveredby[c2]] => y[c1] < y[c2] ( ( cardSequence[initialStacks[stack1*3]] < cardSequence[initialStacks[stack2*3+1]] ) => ( cardSequence[initialStacks[stack1*3]] < cardSequence[initialStacks[stack2*3]] ) ), $ 2 cards are in the middle $ CASE C of Barbara's model forall stack1, stack2 : int(0..16) . ( (stack1 < stack2) /\ $ different stacks and cards in the midle are of the same rank (initialStacks[stack1*3+1] % 13 = initialStacks[stack2*3+1] % 13) ) => $ (y[c1] < y[coveredby[c2] && y[cover[c1]] < y[c2] ) => y[c1] < y[c2] ( ( (cardSequence[initialStacks[stack1*3+1]] < cardSequence[initialStacks[stack2*3+2]]) /\ (cardSequence[initialStacks[stack1*3]] < cardSequence[initialStacks[stack2*3+1]]) ) => ( cardSequence[initialStacks[stack1*3+1]] < cardSequence[initialStacks[stack2*3+1]]) ), $ if two cards have the same rank and one is on top and the other the last of a stack take the top one first $ CASE D in Barbara's model forall stack1, stack2 : int(0..16) . ( (stack1 != stack2) /\ $ different stacks and cards on top of stack1 and bottom of stack2 are of the same rank (initialStacks[stack1*3] % 13 = initialStacks[stack2*3+2] % 13) ) => ( cardSequence[initialStacks[stack1*3]] < cardSequence[initialStacks[stack2*3+2]]), $ ADDs more SEARCH for instance 106 $ one card on top, the other in the middle $ CASE E in barbara's model forall stack1, stack2 : int(0..16) . ( (stack1 != stack2) /\ $ different stacks and cards on top of stack1 and middle of stack2 are of the same rank (initialStacks[stack1*3] % 13 = initialStacks[stack2*3+1] % 13) ) => ( $ y[c1] < y[coveredby[c2] && y[c2] < y[coveredby[c1]] => y[c1] < y[c2] ( (cardSequence[initialStacks[stack1*3]] < cardSequence[initialStacks[stack2*3+2]] ) /\ (cardSequence[initialStacks[stack2*3+1]] < cardSequence[initialStacks[stack1*3+1]] ) ) => ( cardSequence[initialStacks[stack1*3]] < cardSequence[initialStacks[stack2*3+1]]) ), $ one card in middle, other on bottom $ CASE F in barbara's model forall stack1, stack2 : int(0..16) . ( (stack1 != stack2) /\ (initialStacks[stack1*3+1] % 13 = initialStacks[stack2*3+2] % 13) ) => ( $ y[cover[c1]] < y[c2] && y[cover[c2]] < y[c1] => y[c1] < y[c2] ( (cardSequence[initialStacks[stack1*3]] < cardSequence[initialStacks[stack2*3+2]] ) /\ (cardSequence[initialStacks[stack2*3+1]] < cardSequence[initialStacks[stack1*3+1]] ) ) => ( cardSequence[initialStacks[stack1*3+1]] < cardSequence[initialStacks[stack2*3+2]]) )