Download
$ Black Hole
$ 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.0
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)
letting CARDS_ZERO be domain int(0..50)
given initialStacks : matrix indexed by [CARDS_ZERO] of CARDS_NO_ACE
letting CONSECUTIVE_CARD_TABLE =
[ [0,1], [0,14], [0,27], [0,40], [0,51], [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]]
$ 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
such that
$ initial state: the spades ace in in the middle
blackHole[0] = 0,
cardSequence[0] = 0,
allDiff(cardSequence),
allDiff(blackHole),
forAll step : STEPS1 .
table([blackHole[step-1],blackHole[step]], CONSECUTIVE_CARD_TABLE),
$ 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),
$ 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]])
)
This work is licensed under a Creative Commons Attribution 4.0 International License.