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 ) :- WeighingDatum = weighing_data(InfoContent, Left, Right, Table), step( Step, Left, Right, Table, Branches ), findall( WeighingDatum, valid_partition( Coins0, InfoContent, Left, Right, Table ), WeighingData ), sort( WeighingData, OrderedWeighingData ), member( WeighingDatum, OrderedWeighingData ), 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
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