Download
$ 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.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)
$ Cards are numbered 0 -- ace of spades, 1 -- 2 of spades... 13 -- ace of hearts etc.
given initialStacks : matrix indexed by [int(0..50)] 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 the middle
blackHole[0] = 0,
cardSequence[0] = 0,
allDiff(cardSequence),
allDiff(blackHole),
forAll step : STEPS1 .
(|blackHole[step-1] - blackHole[step]| % 13 in {1,12}),
$ 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),
$ 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
false ->
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
false ->
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
false ->
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
false ->
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
false ->
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
false ->
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]])
)