Data.SBV.Examples.Puzzles.Coins

Solves the following puzzle:

You and a friend pass by a standard coin operated vending machine and you decide to get a candy bar.
The price is US $0.95, but after checking your pockets you only have a dollar (US $1) and the machine
only takes coins. You turn to your friend and have this conversation:
  you: Hey, do you have change for a dollar?
  friend: Let's see. I have 6 US coins but, although they add up to a US $1.15, I can't break a dollar.
  you: Huh? Can you make change for half a dollar?
  friend: No.
  you: How about a quarter?
  friend: Nope, and before you ask I cant make change for a dime or nickel either.
  you: Really? and these six coins are all US government coins currently in production? 
  friend: Yes.
  you: Well can you just put your coins into the vending machine and buy me a candy bar, and I'll pay you back?
  friend: Sorry, I would like to but I cant with the coins I have.
What coins are your friend holding?

To be fair, the problem has no solution mathematically. But there is a solution when one takes into account that vending machines typically do not take the 50 cent coins!

Documentation

type Coin = SWord16

We will represent coins with 16-bit words (more than enough precision for coins).

mkCoin :: Int -> Symbolic Coin

Create a coin. The argument Int argument just used for naming the coin. Note that we constrain the value to be one of the valid U.S. coin values as we create it.

combinations :: [a] -> [[a]]

Return all combinations of a sequence of values.

c1 :: [Coin] -> SBool

Constraint 1: Cannot make change for a dollar.

c2 :: [Coin] -> SBool

Constraint 2: Cannot make change for half a dollar.

c3 :: [Coin] -> SBool

Constraint 3: Cannot make change for a quarter.

c4 :: [Coin] -> SBool

Constraint 4: Cannot make change for a dime.

c5 :: [Coin] -> SBool

Constraint 5: Cannot make change for a nickel

c6 :: [Coin] -> SBool

Constraint 6: Cannot buy the candy either. Here's where we need to have the extra knowledge that the vending machines do not take 50 cent coins.

puzzle :: IO SatResult

Solve the puzzle. We have:

>>> puzzle
Satisfiable. Model:
  c1 = 50 :: Word16
  c2 = 25 :: Word16
  c3 = 10 :: Word16
  c4 = 10 :: Word16
  c5 = 10 :: Word16
  c6 = 10 :: Word16

i.e., your friend has 4 dimes, a quarter, and a half dollar.