sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Documentation.SBV.Examples.Puzzles.Coins

Description

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.
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!

Synopsis

# Documentation

type Coin = SWord16 Source #

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

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]] Source #

Return all combinations of a sequence of values.

c1 :: [Coin] -> SBool Source #

Constraint 1: Cannot make change for a dollar.

c2 :: [Coin] -> SBool Source #

Constraint 2: Cannot make change for half a dollar.

c3 :: [Coin] -> SBool Source #

Constraint 3: Cannot make change for a quarter.

c4 :: [Coin] -> SBool Source #

Constraint 4: Cannot make change for a dime.

c5 :: [Coin] -> SBool Source #

Constraint 5: Cannot make change for a nickel

c6 :: [Coin] -> SBool Source #

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.

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.