# The Counterfeit Coin Puzzle

## Problem Definition

We are given 12 apparently identical coins - one of which is counterfeit. We know that the counterfeit has a different weight from the others, but we don't know if it's heavier or lighter.

### Task:

Devise a procedure to identify any counterfeit coin using a balance to take up to three comparative weighings.

## Strategy

The information from three suitable weighings will make all but one of the coins, which are untested initially, known_true. There are three alternative deductions that make a coin known_true:

- if it is not_heavy and not_light – having been on both the comparatively lighter and heavier sides of imbalances;
- if it was excluded from an imbalance;
- if it was included in a balanced weighing.

After three weighings there must be exactly one coin, the counterfeit, which is not known_true. If the counterfeit is not known_true and not_heavy we deduce that it must be light. If it is not known_true and not_light, it must be heavy.

We use a generate-and-test method as follows:

- Create the set of all possible counterfeits: 12 coins × 2 weights ;
- Devise a procedure that can identify the first counterfeit coin;
- Show that the same procedure works for every other counterfeit coin.

## Entry Point

#### go

is the entry point. It solves the puzzle, then uses a DCG to pretty-print the resulting procedure.

go :- coins_puzzle( Procedure ), phrase( general_explanation( Procedure ), Chars ), put_chars( Chars ).

#### coins_puzzle( ?Procedure )

generates the set of all possible counterfeit coins and finds, or proves, that `Procedure` can identify them all.

coins_puzzle( Procedure ) :- coins( Coins ), counterfeit( Counterfeit, Coin, Weight ), findall( Counterfeit, (member(Coin,Coins), counterfeit_weight(Weight)), Counterfeits ), coins_puzzle_solution( Counterfeits, Procedure ). coins_puzzle_solution( [], _Procedure ). coins_puzzle_solution( [Counterfeit|Counterfeits], Procedure ) :- solve_coins( Counterfeit, Procedure ), coins_puzzle_solution( Counterfeits, Procedure ).

A procedure is either *done*, identifying a particular coin and whether
it is heavy or light, or it is a *step*.

A *step* defines the coins to be placed on the `Left` and
`Right` pans, with the residue remaining on the
`Table`, and three `Branches`, one of which will
be chosen depending on the outcome of the weighing.

step( step(Left,Right,Table,Branches), Left, Right, Table, Branches).

The `Branches` are three procedures equating to:

- > (left pan heavier),
- < (right pan heavier) and
- = (pans balance).

branch( >, branches(_Equal, GT, _LT), GT ). branch( <, branches(_Equal, _GT, LT), LT ). branch( =, branches(Equal, _GT, _LT), Equal ).

The counterfeit is defined by its number and whether it is heavy or light.

counterfeit( counterfeit(Coin, HeavyOrLight), Coin, HeavyOrLight ). coins( [1,2,3,4,5,6,7,8,9,10,11,12] ). counterfeit_weight( heavy ). counterfeit_weight( light ).

A *coin collection* comprises four `part`

s (subsets): the `known_true`

, `not_heavy`

, `not_light`

and `untested`

sets of coins.

part( known_true, collection(Coins,_,_,_), Coins ). part( not_heavy, collection(_,Coins,_,_), Coins ). part( not_light, collection(_,_,Coins,_), Coins ). part( untested, collection(_,_,_,Coins), Coins ).

## Solution

#### solve_coins( +Counterfeit, ?Procedure )

holds when `Procedure` can correctly identify the `Counterfeit` coin. Beginning with a *start* collection, in which all the coins are untested, the `Procedure` comprises three steps.

For each step, a weighing is made and a *branch* is made in the `Procedure`, depending on the result of the weighing.

After three steps, the `Procedure` must have reached the *end* condition.

Finally, an assertion (redundant test) ensures that the `Procedure` has found the correct *end* condition.

solve_coins( Counterfeit, Procedure ) :- start( Coins0 ), assay( Counterfeit, Coins0, Procedure, Branch1, Coins1 ), assay( Counterfeit, Coins1, Branch1, Branch2, Coins2 ), assay( Counterfeit, Coins2, Branch2, done(Coin, HeavyOrLight), Coins3 ), end( Coins3, Coin, HeavyOrLight ), counterfeit( Counterfeit, Coin, HeavyOrLight ). start( Coins ) :- coins( Untested ), part( untested, Coins, Untested ), part( not_heavy, Coins, [] ), part( not_light, Coins, [] ), part( known_true, Coins, [] ). end( Coins, Coin, HeavyOrLight ) :- part( untested, Coins, [] ), part( not_heavy, Coins, Light ), part( not_light, Coins, Heavy ), end_result( Heavy, Light, Coin, HeavyOrLight ). end_result( [Coin], [], Coin, heavy ). end_result( [], [Coin], Coin, light ).

### Simulating the weighing process

#### assay( +Counterfeit, +Coins0, ?Step, ?Branch, ?Coins1 )

holds when the appropriate `Branch` from `Step` is chosen by comparing the weights of two coin collections taken from the full set of coins: `Coins0`. `Coins1` is the full set of coins updated with the inferences drawn from the weighing, where `Counterfeit` is used to determine the result of the weighing.

This predicate applies the critical insight into the solution of this puzzle: we have 24 (12 × 2) possible inputs to the procedure, with only 27 (3 × 3 × 3) possible outcomes from the weighings.

Therefore, it is clear that each weighing must have a very high information content. Choosing which weighing to make by estimating the available information content makes the problem tractable.

assay( Counterfeit, Coins0, Step, Branch, Coins ) :- step( Step, Left, Right, Table, Branches ), partition( Coins0, Left, Right, Table ), balance( Left, Right, Counterfeit, Result ), draw_inferences( Result, Left, Right, Table, Coins ), branch( Result, Branches, Branch ).

#### balance( +Left, +Right, +Counterfeit, ?Result )

holds when `Result` simulates the outcome of testing the coin collections
`Left` and `Right` with a balance, where either
may contain the `Counterfeit` coin.

balance( Left, Right, Counterfeit, Result ):- counterfeit( Counterfeit, Coin, Weight ), ( contains_coin( Left, Coin ) -> balance_result( Weight, normal, Result ) ; contains_coin( Right, Coin ) -> balance_result( normal, Weight, Result ) ; otherwise -> Result = '=' ). balance_result( light, normal, < ). balance_result( heavy, normal, > ). balance_result( normal, heavy, < ). balance_result( normal, light, > ).

### Choosing which coins to weigh

#### partition( +Coins, ?Left, ?Right, ?Table )

holds when `Coins` is partitioned into three collections:
`Left` side, `Right` side and `Table`.

Operationally, alternative valid partitions are selected in order of reducing information content.

partition( Coins, Left, Right, Table ) :- Partition = ptn(Info,Left,Right,Table), findall( Partition, valid_partition(Coins, Info, Left, Right, Table), Partitions ), sort( Partitions, OrderedPartitions ), member( Partition, OrderedPartitions ).

#### valid_partition( +Coins, ?Content, ?Left, ?Right, ?Table )

holds when `Coins` can be partitioned into three collections:
`Left` side, `Right` side and `Table`;
with the information content of the partition given by
`Content`.

The definition of a valid_partition ensures that:

`Left`and`Right`must have the same number of coins (at least one);`Left`cannot contain any known_true coins, because adding true coins to both sides creates redundant comparisons;- Comparisons between mixtures of coins where only the choice of pans is different are equivalent, so a partial order (≥) on mixtures of coins is used to eliminate some redundant comparisons.

valid_partition( Coins, Content, Left, Right, Table ):- part( known_true, Left, [] ), selection( Coins, Left, Coins1, LeftSum, LeftInfo ), selection( Coins1, Right, Table, RightSum, RightInfo ), LeftSum =:= RightSum, LeftSum @>= RightSum, table_information( Table, TableInfo ), sum( [LeftInfo,RightInfo,TableInfo], Content ).

#### selection( +Coins, ?Sample, ?Residue, ?Sum, ?Content )

holds when `Coins` is partitioned into two collections:
`Sample` and `Residue`. `Sum` is
used as both a fingerprint for the mixture of coins in `Sample`
and a representation of the number of coins in `Sample`.
`Content` estimates the information-content of `Sample`.

selection( Coins, Sample, Residue, Sum, Content ) :- Sum = Count1+Count2+Count3+Count4, select_coins( not_heavy, Coins, Sample, Residue, Count1 ), select_coins( not_light, Coins, Sample, Residue, Count2 ), select_coins( untested, Coins, Sample, Residue, Count3 ), select_coins( known_true, Coins, Sample, Residue, Count4 ), Sum >= 1, Sum =< 6, information_content( [Count1,Count2,Count3,Count4], Content ).

#### table_information( +Coins, ?Content )

holds when `Coins` has 'information content'
`Content`.

table_information( Coins, Content ) :- count_coins( not_heavy, Coins, Count1 ), count_coins( not_light, Coins, Count2 ), count_coins( untested, Coins, Count3 ), count_coins( known_true, Coins, Count4 ), information_content( [Count1,Count2,Count3,Count4], Content ). count_coins( Part, Coins, Count ) :- part( Part, Coins, Selection ), length( Selection, Count ).

### Updating what is known about the coins

#### draw_inferences( +Result, +Left, +Right, +Table, ?Coins )

holds when `Result` is one of:

- > (imbalance – left pan heavier),
- < (imbalance – right pan heavier) or
- = (pans balanced)

from taking a weighing with the coin collections: `Left`, `Right` and `Table`.

`Coins` is derived from this information using the following rules:

- If the pans are unbalanced then only the previously untested or not_heavy coins on the lighter side of the balance are now not_heavy. Similarly, only the previously untested or not_light coins on the heavier side of the balance are now not_light. All the coins on the table are now known_true.
- If the pans balance then all the coins weighed are known_true, with the coins on the
`Table`left in their prior states.

draw_inferences( <, Left, Right, Table, Coins ) :- imbalance_inferences( Left, Right, Table, Coins ). draw_inferences( >, Left, Right, Table, Coins ) :- imbalance_inferences( Right, Left, Table, Coins ). draw_inferences( =, Left, Right, Table, Coins ) :- becomes( [all(Left),known_true(Table),all(Right)], known_true( Coins ) ), becomes( untested(Table), untested(Coins) ), becomes( not_heavy(Table), not_heavy(Coins) ), becomes( not_light(Table), not_light(Coins) ).

#### imbalance_inferences( +Lighter, +Heavier, +Table, ?Coins )

holds when:

- Only the untested or not_heavy coins in
`Lighter`are not_heavy in`Coins`; - Only the untested or not_light coins in
`Heavier`are not_light in`Coins`; - All the other coins in
`Lighter`and`Heavier`and all the coins in`Table`are known_true in`Coins`;

There are no untested coins in `Coins`.

imbalance_inferences( Lighter, Heavier, Table, Coins ) :- becomes( [untested(Lighter),not_heavy(Lighter)], not_heavy(Coins) ), becomes( [untested(Heavier),not_light(Heavier)], not_light(Coins) ), becomes( [ known_true(Lighter), not_light(Lighter), known_true(Heavier), not_heavy(Heavier), all(Table) ], known_true(Coins) ), part( untested, Coins, [] ).

#### becomes( +CollectionA, ?CollectionB )

`CollectionA` becomes (part) `CollectionB` when `CollectionB` comprises the same coins as `CollectionA`.

becomes( CollectionA, CollectionB ) :- unfolded( CollectionA, Coins ), unfolded( CollectionB, Coins ).

#### unfolded( +Collection, ?Coins )

holds when (part) `Collection` comprises `Coins`.

unfolded( not_light(Collection), Coins ) :- part( not_light, Collection, Coins ). unfolded( not_heavy(Collection), Coins ) :- part( not_heavy, Collection, Coins ). unfolded( known_true(Collection), Coins ) :- part( known_true, Collection, Coins ). unfolded( untested(Collection), Coins ) :- part( untested, Collection, Coins ). unfolded( all(Collection), Coins ) :- collection_to_set( Collection, Coins ). unfolded( [Item|Items], Coins ) :- unfolded( Item, Value ), unfolded1( Items, Value, Coins ). unfolded1( [], Coins, Coins ). unfolded1( [Item|Items], Value, Coins ) :- unfolded( Item, Value0 ), ord_union( Value0, Value, Value1 ), unfolded1( Items, Value1, Coins ).

## Definite Clause Grammar

The following DCG presents the method for finding the counterfeit coin as a structured procedure.

general_explanation( Procedure ) --> "Number the coins 1..12", newline, explanation( Procedure, 0 ). explanation( done(Coin, Weight), N ) --> tab( N ), "Conclude that the counterfeit coin is number ", literal( Coin ), ", which is ", literal( Weight ), newline. explanation( Step, N ) --> {step( Step, Left, Right, Table, Branches )}, tab( N ), "BEGIN", newline, tab( N ), "Put ", literal( Left ), " on the left-hand pan", newline, tab( N ), "Put ", literal( Right ), " on the right-hand pan", newline, tab( N ), "Leaving ", literal( Table ), " on the table", newline, branches_explained( Branches, N ), tab( N ), "END", newline. branches_explained( Branches, N ) --> next_step_explained( <, Branches, N ), next_step_explained( >, Branches, N ), next_step_explained( =, Branches, N ). next_step_explained( Result, Branch, N ) --> {branch( Result, Branch, Step )}, ( {var(Step)} -> "" | {nonvar(Step)} -> tab( N ), "If the ", literal( Result ), " then:", newline, explanation( Step, s(N) ) ). literal( 0 ) --> "0". literal( 1 ) --> "1". literal( 2 ) --> "2". literal( 3 ) --> "3". literal( 4 ) --> "4". literal( 5 ) --> "5". literal( 6 ) --> "6". literal( 7 ) --> "7". literal( 8 ) --> "8". literal( 9 ) --> "9". literal( 10 ) --> "10". literal( 11 ) --> "11". literal( 12 ) --> "12". literal( true ) --> "true". literal( heavy ) --> "heavy". literal( light ) --> "light". literal( = ) --> "pans balance". literal( < ) --> "right-hand pan is heavier". literal( > ) --> "left-hand pan is heavier". literal( Collection ) --> {collection_to_set( Collection , [H|T] )}, literal_set( T, H ). literal_set( [], Number ) --> "the coin numbered ", literal( Number ). literal_set( [H|T], Number ) --> "the coins numbered ", literal( Number ), literal_set1( T, H ). literal_set1( [], Number ) --> " and ", literal( Number ). literal_set1( [H|T], Number ) --> ", ", literal( Number ), literal_set1( T, H ). tab( 0 ) --> "". tab( s(N) ) --> " ", tab( N ). newline --> " ".

### Utility Predicates

#### contains_coin( ?Collection, ?Coin )

holds when `Coin` is a member of `Collection`.

contains_coin( Collection, Coin ) :- part( _Part, Collection, Coins ), member( Coin, Coins ).

#### collection_to_set( +Collection, ?Set )

holds when `Set` is the distributed union of the `known_true`

,
`not_heavy`

, `not_light`

and `untested`

ordsets comprising `Collection`.

collection_to_set( Collection, Set ) :- part( known_true, Collection, KnownTrue ), part( not_heavy, Collection, NotHeavy ), part( not_light, Collection, NotLight ), part( untested, Collection, Untested ), ord_union( [KnownTrue,NotHeavy,NotLight,Untested], Set ).

### Information Content

#### information_content( +Counts, ?Content )

holds when `Content` is the cumulative negative entropy of `Counts`. A reduction in entropy equates to a gain in information.

information_content( Counts, Content ) :- information_content1( Counts, 0, Content ). information_content1( [], Content, Content ). information_content1( [Count|Counts], Content0, Content ):- coins_entropy( Count, Entropy ), Content1 is Content0-Entropy, information_content1( Counts, Content1, Content ).

#### coins_entropy( ?N, ?Entropy )

holds when `Entropy` estimates the entropy of a sample of `N` coins.

`Entropy` = P log_{2}(^{1}⁄_{P}), where
P = `N`÷12.

coins_entropy( 0, 0.0 ). coins_entropy( 1, 0.2987 ). coins_entropy( 2, 0.4308 ). coins_entropy( 3, 0.5 ). coins_entropy( 4, 0.5283 ). coins_entropy( 5, 0.5263 ). coins_entropy( 6, 0.5 ). coins_entropy( 7, 0.4536 ). coins_entropy( 8, 0.39 ). coins_entropy( 9, 0.3113 ). coins_entropy( 10, 0.2192 ). coins_entropy( 11, 0.1151 ). coins_entropy( 12, 0.0 ).

#### select_coins( +Part, +Coins, ?Sample, ?Residue, ?N )

holds when `N` coins from `Part` of `Coins` form `Part` of `Sample`,
with the remainder forming `Part` of `Residue`.

select_coins( Part, Coins, Sample, Residue, Count ) :- part( Part, Coins, Input ), part( Part, Sample, Selection ), part( Part, Residue, Remainder ), select_n( Count, Input, Selection, Remainder ). select_n( 0, In, [], In ). select_n( 1, [A|Suffix], [A], Suffix ). select_n( 2, [A,B|Suffix], [A,B], Suffix ). select_n( 3, [A,B,C|Suffix], [A,B,C], Suffix ). select_n( 4, [A,B,C,D|Suffix], [A,B,C,D], Suffix ). select_n( 5, [A,B,C,D,E|Suffix], [A,B,C,D,E], Suffix ). select_n( 6, [A,B,C,D,E,F|Suffix], [A,B,C,D,E,F], Suffix ).

Load a small library of Puzzle Utilities.

:- ensure_loaded( misc ).

Use the ordsets library.

:- use_module( library(ordsets), [ord_union/2,ord_union/3] ).

The code is available as plain text here.

## Output

Number the coins 1..12 BEGIN Put the coins numbered 1, 2, 3 and 4 on the left-hand pan Put the coins numbered 5, 6, 7 and 8 on the right-hand pan Leaving the coins numbered 9, 10, 11 and 12 on the table If the right-hand pan is heavier then: BEGIN Put the coins numbered 1, 2, 5 and 6 on the left-hand pan Put the coins numbered 3, 7, 9 and 10 on the right-hand pan Leaving the coins numbered 4, 8, 11 and 12 on the table If the right-hand pan is heavier then: BEGIN Put the coins numbered 1 and 7 on the left-hand pan Put the coins numbered 3 and 4 on the right-hand pan Leaving the coins numbered 2, 5, 6, 8, 9, 10, 11 and 12 on the table If the right-hand pan is heavier then: Conclude that the counterfeit coin is number 1, which is light If the left-hand pan is heavier then: Conclude that the counterfeit coin is number 7, which is heavy If the pans balance then: Conclude that the counterfeit coin is number 2, which is light END If the left-hand pan is heavier then: BEGIN Put the coins numbered 3 and 5 on the left-hand pan Put the coins numbered 1 and 2 on the right-hand pan Leaving the coins numbered 4, 6, 7, 8, 9, 10, 11 and 12 on the table If the right-hand pan is heavier then: Conclude that the counterfeit coin is number 3, which is light If the left-hand pan is heavier then: Conclude that the counterfeit coin is number 5, which is heavy If the pans balance then: Conclude that the counterfeit coin is number 6, which is heavy END If the pans balance then: BEGIN Put the coins numbered 4 and 8 on the left-hand pan Put the coins numbered 1 and 2 on the right-hand pan Leaving the coins numbered 3, 5, 6, 7, 9, 10, 11 and 12 on the table If the right-hand pan is heavier then: Conclude that the counterfeit coin is number 4, which is light If the left-hand pan is heavier then: Conclude that the counterfeit coin is number 8, which is heavy END END If the left-hand pan is heavier then: BEGIN Put the coins numbered 1, 2, 5 and 6 on the left-hand pan Put the coins numbered 3, 7, 9 and 10 on the right-hand pan Leaving the coins numbered 4, 8, 11 and 12 on the table If the right-hand pan is heavier then: BEGIN Put the coins numbered 3 and 5 on the left-hand pan Put the coins numbered 1 and 2 on the right-hand pan Leaving the coins numbered 4, 6, 7, 8, 9, 10, 11 and 12 on the table If the right-hand pan is heavier then: Conclude that the counterfeit coin is number 5, which is light If the left-hand pan is heavier then: Conclude that the counterfeit coin is number 3, which is heavy If the pans balance then: Conclude that the counterfeit coin is number 6, which is light END If the left-hand pan is heavier then: BEGIN Put the coins numbered 1 and 7 on the left-hand pan Put the coins numbered 3 and 4 on the right-hand pan Leaving the coins numbered 2, 5, 6, 8, 9, 10, 11 and 12 on the table If the right-hand pan is heavier then: Conclude that the counterfeit coin is number 7, which is light If the left-hand pan is heavier then: Conclude that the counterfeit coin is number 1, which is heavy If the pans balance then: Conclude that the counterfeit coin is number 2, which is heavy END If the pans balance then: BEGIN Put the coins numbered 4 and 8 on the left-hand pan Put the coins numbered 1 and 2 on the right-hand pan Leaving the coins numbered 3, 5, 6, 7, 9, 10, 11 and 12 on the table If the right-hand pan is heavier then: Conclude that the counterfeit coin is number 8, which is light If the left-hand pan is heavier then: Conclude that the counterfeit coin is number 4, which is heavy END END If the pans balance then: BEGIN Put the coins numbered 9, 10 and 11 on the left-hand pan Put the coins numbered 1, 2 and 3 on the right-hand pan Leaving the coins numbered 4, 5, 6, 7, 8 and 12 on the table If the right-hand pan is heavier then: BEGIN Put the coin numbered 9 on the left-hand pan Put the coin numbered 10 on the right-hand pan Leaving the coins numbered 1, 2, 3, 4, 5, 6, 7, 8, 11 and 12 on the table If the right-hand pan is heavier then: Conclude that the counterfeit coin is number 9, which is light If the left-hand pan is heavier then: Conclude that the counterfeit coin is number 10, which is light If the pans balance then: Conclude that the counterfeit coin is number 11, which is light END If the left-hand pan is heavier then: BEGIN Put the coin numbered 9 on the left-hand pan Put the coin numbered 10 on the right-hand pan Leaving the coins numbered 1, 2, 3, 4, 5, 6, 7, 8, 11 and 12 on the table If the right-hand pan is heavier then: Conclude that the counterfeit coin is number 10, which is heavy If the left-hand pan is heavier then: Conclude that the counterfeit coin is number 9, which is heavy If the pans balance then: Conclude that the counterfeit coin is number 11, which is heavy END If the pans balance then: BEGIN Put the coin numbered 12 on the left-hand pan Put the coin numbered 1 on the right-hand pan Leaving the coins numbered 2, 3, 4, 5, 6, 7, 8, 9, 10 and 11 on the table If the right-hand pan is heavier then: Conclude that the counterfeit coin is number 12, which is light If the left-hand pan is heavier then: Conclude that the counterfeit coin is number 12, which is heavy END END END