In [48]:

    

import itertools
import Numberjack

RANKS = {
  0: 'A',
  1: '2',
  2: '3',
  3: '4',
  4: '5',
  5: '6',
  6: '7',
  7: '8',
  8: '9',
  9: '10',
  10: 'J',
  11: 'Q',
  12: 'K',
}
TO_RANK = dict([(v, k) for k, v in RANKS.items()])
SUITS = {
  0: 'hearts',
  1: 'diamonds',
  2: 'clubs',
  3: 'spades',
}
TO_SUIT = dict([(v[0], k) for k, v in SUITS.items()])

class CardVariable(object):
  def __init__(self, i):
    self.num = i
    self.rank = Numberjack.Variable(13, '#%s rank' % i)
    self.suit = Numberjack.Variable(4, '#%s suit' % i)

  def id(self):
    return self.suit * len(RANKS) + self.rank

  def __str__(self):
    return '#%s %s of %s' % (
      self.num,
      RANKS[self.rank.get_value()],
      SUITS[self.suit.get_value()]
    )

class CardValue(object):
  def __init__(self, card):
    self.suit = TO_SUIT[card[0]]
    self.rank = TO_RANK[card[1:]]

model = Numberjack.Model()

cards = [CardVariable(i) for i in range(1, 5+1)]
model.add(Numberjack.AllDiff([c.id() for c in cards]))

def score_correct_rank(guesses):
  return Numberjack.Sum(guesses[i].rank == cards[i].rank for i in range(len(cards)))

def score_correct_rank_wrong_position(guesses):
  sums = []
  for i in range(len(guesses)):
    sums.append(
      # First, confirm wrong position.
      (guesses[i].rank != cards[i].rank) *
      # Second, see if this guess matches any other cards.
      Numberjack.Disjunction(list(
        guesses[i].rank == cards[j].rank
        for j in itertools.chain(range(0, i), range(i+1, len(cards)))
      ))
    )
  return Numberjack.Sum(sums)

def score_correct_suit(guesses):
  return Numberjack.Sum(guesses[i].suit == cards[i].suit for i in range(len(cards)))

def score_correct_suit_wrong_position(guesses):
  exprs = []
  for x in SUITS:
    exprs.append(Numberjack.Sum(cards[i].suit == x for i in range(len(cards))))
  return Numberjack.Sum(exprs) - score_correct_suit(guesses)

def guess(*guesses, score=[]):
  cards = [CardValue(g) for g in guesses]
  model.add(
    score_correct_rank(cards) == score[0],
    score_correct_rank_wrong_position(cards) == score[1],
    score_correct_suit(cards) == score[2],
    # Doesn't work:
    # score_correct_suit_wrong_position(cards) == score[3],
  )

guess('s2', 'h3', 'dA', 'cK',  'sQ', score=[0, 3, 1, 2])
guess('h7', 'd8', 'c9', 's10', 'hJ', score=[0, 1, 1, 3])
guess('d4', 'c5', 'h6', 'h7',  'd7', score=[1, 1, 1, 2])
guess('hQ', 'h7', 'hK', 'c7',  's3', score=[3, 0, 3, 1])
guess('d7', 'hK', 'h2', 'h7',  'sA', score=[3, 1, 1, 2])
# A:  'hQ', 's7', 'h2', 'c7',  'cA'

solver = model.load('Mistral')
print(str(model))
solver.solve()

if solver.is_unsat():
  print('Impossible')
else:
  for c in cards:
    print(str(c))


    

    




assign:
  #1 suit in {0..3}
  #1 rank in {0,2..5,7..12}
  #2 suit in {0..3}
  #2 rank in {0,1,3..6,8..12}
  #3 suit in {0..3}
  #3 rank in {1..7,9..12}
  #4 suit in {0..3}
  #4 rank in {0..8,10,11}
  #5 suit in {0..3}
  #5 rank in {0..9,12}
  
subject to:
  AllDiff((13*#1 suit + #1 rank), (13*#2 suit + #2 rank), (13*#3 suit + #3 rank), (13*#4 suit + #4 rank), (13*#5 suit + #5 rank))
  (((#1 rank == 1) + (#2 rank == 2) + (#3 rank == 0) + (#4 rank == 12) + (#5 rank == 11)) == 0)
  ((((#1 rank != 1) * OR((#2 rank == 1), (#3 rank == 1), (#4 rank == 1), (#5 rank == 1))) + ((#2 rank != 2) * OR((#1 rank == 2), (#3 rank == 2), (#4 rank == 2), (#5 rank == 2))) + ((#3 rank != 0) * OR((#1 rank == 0), (#2 rank == 0), (#4 rank == 0), (#5 rank == 0))) + ((#4 rank != 12) * OR((#1 rank == 12), (#2 rank == 12), (#3 rank == 12), (#5 rank == 12))) + ((#5 rank != 11) * OR((#1 rank == 11), (#2 rank == 11), (#3 rank == 11), (#4 rank == 11)))) == 3)
  (((#1 suit == 3) + (#2 suit == 0) + (#3 suit == 1) + (#4 suit == 2) + (#5 suit == 3)) == 1)
  (((#1 rank == 6) + (#2 rank == 7) + (#3 rank == 8) + (#4 rank == 9) + (#5 rank == 10)) == 0)
  ((((#1 rank != 6) * OR((#2 rank == 6), (#3 rank == 6), (#4 rank == 6), (#5 rank == 6))) + ((#2 rank != 7) * OR((#1 rank == 7), (#3 rank == 7), (#4 rank == 7), (#5 rank == 7))) + ((#3 rank != 8) * OR((#1 rank == 8), (#2 rank == 8), (#4 rank == 8), (#5 rank == 8))) + ((#4 rank != 9) * OR((#1 rank == 9), (#2 rank == 9), (#3 rank == 9), (#5 rank == 9))) + ((#5 rank != 10) * OR((#1 rank == 10), (#2 rank == 10), (#3 rank == 10), (#4 rank == 10)))) == 1)
  (((#1 suit == 0) + (#2 suit == 1) + (#3 suit == 2) + (#4 suit == 3) + (#5 suit == 0)) == 1)
  (((#1 rank == 3) + (#2 rank == 4) + (#3 rank == 5) + (#4 rank == 6) + (#5 rank == 6)) == 1)
  ((((#1 rank != 3) * OR((#2 rank == 3), (#3 rank == 3), (#4 rank == 3), (#5 rank == 3))) + ((#2 rank != 4) * OR((#1 rank == 4), (#3 rank == 4), (#4 rank == 4), (#5 rank == 4))) + ((#3 rank != 5) * OR((#1 rank == 5), (#2 rank == 5), (#4 rank == 5), (#5 rank == 5))) + ((#4 rank != 6) * OR((#1 rank == 6), (#2 rank == 6), (#3 rank == 6), (#5 rank == 6))) + ((#5 rank != 6) * OR((#1 rank == 6), (#2 rank == 6), (#3 rank == 6), (#4 rank == 6)))) == 1)
  (((#1 suit == 1) + (#2 suit == 2) + (#3 suit == 0) + (#4 suit == 0) + (#5 suit == 1)) == 1)
  (((#1 rank == 11) + (#2 rank == 6) + (#3 rank == 12) + (#4 rank == 6) + (#5 rank == 2)) == 3)
  ((((#1 rank != 11) * OR((#2 rank == 11), (#3 rank == 11), (#4 rank == 11), (#5 rank == 11))) + ((#2 rank != 6) * OR((#1 rank == 6), (#3 rank == 6), (#4 rank == 6), (#5 rank == 6))) + ((#3 rank != 12) * OR((#1 rank == 12), (#2 rank == 12), (#4 rank == 12), (#5 rank == 12))) + ((#4 rank != 6) * OR((#1 rank == 6), (#2 rank == 6), (#3 rank == 6), (#5 rank == 6))) + ((#5 rank != 2) * OR((#1 rank == 2), (#2 rank == 2), (#3 rank == 2), (#4 rank == 2)))) == 0)
  (((#1 suit == 0) + (#2 suit == 0) + (#3 suit == 0) + (#4 suit == 2) + (#5 suit == 3)) == 3)
  (((#1 rank == 6) + (#2 rank == 12) + (#3 rank == 1) + (#4 rank == 6) + (#5 rank == 0)) == 3)
  ((((#1 rank != 6) * OR((#2 rank == 6), (#3 rank == 6), (#4 rank == 6), (#5 rank == 6))) + ((#2 rank != 12) * OR((#1 rank == 12), (#3 rank == 12), (#4 rank == 12), (#5 rank == 12))) + ((#3 rank != 1) * OR((#1 rank == 1), (#2 rank == 1), (#4 rank == 1), (#5 rank == 1))) + ((#4 rank != 6) * OR((#1 rank == 6), (#2 rank == 6), (#3 rank == 6), (#5 rank == 6))) + ((#5 rank != 0) * OR((#1 rank == 0), (#2 rank == 0), (#3 rank == 0), (#4 rank == 0)))) == 1)
  (((#1 suit == 1) + (#2 suit == 0) + (#3 suit == 0) + (#4 suit == 0) + (#5 suit == 3)) == 1)
  
#1 Q of hearts
#2 7 of spades
#3 2 of hearts
#4 7 of clubs
#5 A of clubs

In [ ]: