% 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 3 comparative weighings. % % Strategy % % The information from three suitable weighings will make all but one of the % 'coins', which are unknown 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 'light' % and 'heavy' 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 'true'. If the counterfeit is not true and 'not heavy' we deduce that % it must be light. If it is not 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 x 2 weights ; % Devise a procedure that can identify the first counterfeit coin; % Recursively show that the same procedure works for every other % counterfeit. % Entry Point % go/0 is the entry point: it solves the puzzle, then uses a DCG to % "pretty print" the resultant procedure. go :- coins_puzzle( Procedure ), phrase( general_explanation( Procedure ), Chars ), put_chars( Chars ). % coins_puzzle( ?Procedure ) generates the set of all possible % 'counterfeits' 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 ). % Constants coins( [1,2,3,4,5,6,7,8,9,10,11,12] ). counterfeit_weight( heavy ). counterfeit_weight( light ). % Data Abstraction % We define a 'coin collection' as comprising sets of coins which are: % known_true, not_heavy, not_light or (completely) unknown. known_true( coins(KnownTrue,_NotHeavy,_NotLight,_Unknown), KnownTrue ). not_heavy( coins(_KnownTrue,NotHeavy,_NotLight,_Unknown), NotHeavy ). not_light( coins(_KnownTrue,_NotHeavy,NotLight,_Unknown), NotLight ). unknown_( coins(_KnownTrue,_NotHeavy,_NotLight,Unknown), Unknown ). % The name of unknown_/2 is decorated with an underscore to avoid conflict % with the built-in predicate unknown/2. part_collection( Collection, Coins ):- known_true( Collection, Coins ). part_collection( Collection, Coins ):- not_heavy( Collection, Coins ). part_collection( Collection, Coins ):- not_light( Collection, Coins ). part_collection( Collection, Coins ):- unknown_( Collection, Coins ). % A procedure is either: % - 'done' identifying a particular coin and whether it is 'heavy' or % 'light'; % or % - a 'step' defining the weighing of Left (pan), Right (pan) and Table % (residue); 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), Equal ). branch( <, branches(_Equal, _GT, LT), LT ). branch( >, branches(_Equal, GT, _LT), GT ). % The counterfeit coin is defined by its number and whether it is heavy % or light. counterfeit( counterfeit(Coin, HeavyOrLight), Coin, HeavyOrLight ). % 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 unknown, the Procedure comprises three % 'steps'. % % For each step a 'weighing' is made and, depending on the result of % the weighing, a 'branch' is made in the Procedure. % % 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( Unknown ), unknown_( Coins, Unknown ), not_heavy( Coins, [] ), not_light( Coins, [] ), known_true( Coins, [] ). end( Coins, Coin, HeavyOrLight ) :- unknown_( Coins, [] ), not_heavy( Coins, Light ), not_light( Coins, Heavy ), end_result( Heavy, Light, Coin, HeavyOrLight ). end_result( [Coin], [], Coin, heavy ). end_result( [], [Coin], Coin, light ). % 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. % 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 x 2) possible inputs to the procedure with only 27 % (3 x 3 x 3) possible outcomes from the weighings; so it is clear that % each weighing must have a very high 'information content'. Choosing a % weighing by '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 ). % draw_inferences( Result, Left, Right, Table, Coins ) holds when % Result is one of: % > (unbalanced - left pan heavier), % < (unbalanced - 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 unknown or not_heavy % coins on the 'light' side of the balance are now not_heavy. Similarly, only % the previously unknown or not_light coins on the 'heavy' 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 only % the coins on the Table left in (partially) unknown states. draw_inferences( =, Left, Right, Table, Coins ) :- draw_balanced_inferences( Left, Right, Table, Coins ). draw_inferences( <, Left, Right, Table, Coins ) :- draw_unbalanced_inferences( Left, Right, Table, Coins ). draw_inferences( >, Left, Right, Table, Coins ) :- draw_unbalanced_inferences( Right, Left, Table, Coins ). draw_balanced_inferences( Left, Right, Table, Coins ) :- inference( [ unknown(Left), known_true( Left ), not_heavy( Left ), not_light( Left ), known_true( Table ), known_true( Right ), unknown( Right ), not_heavy( Right ), not_light( Right ) ], known_true( Coins ) ), inference( unknown(Table), unknown(Coins) ), inference( not_heavy(Table), not_heavy(Coins) ), inference( not_light(Table), not_light(Coins) ). draw_unbalanced_inferences( Light, Heavy, Table, Coins ) :- inference( [unknown(Light),not_heavy(Light)], not_heavy(Coins) ), inference( [unknown(Heavy),not_light(Heavy)], not_light(Coins) ), inference( [ known_true(Light), not_light(Light), known_true(Heavy), not_heavy(Heavy), unknown(Table), known_true(Table), not_heavy(Table), not_light(Table) ], known_true(Coins) ), unknown_( Coins, [] ). % valid_partition( +Coins, ?Content, ?Left, ?Right, ?Table ) holds when % Coins can be partitioned into three collections: Left and Right and Table, % with the 'information content' of the partition is given by Content. % The definition of a 'valid partition' is fairly naive: - 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. valid_partition( Coins, Content, Left, Right, Table ):- Sizes = [ LNotHeavySize, LNotLightSize, LUnknownSize, RTrueSize, RNotHeavySize, RNotLightSize, RUnknownSize, TableTrueSize, TableLightSize, TableHeavySize, TableUnknownSize ], not_light( Coins, HeavyAll ), not_heavy( Coins, LightAll ), known_true( Coins, TrueAll ), unknown_( Coins, UnknownAll ), not_light( Left, LNotLight ), not_heavy( Left, LNotHeavy ), known_true( Left, [] ), % LTrue = 0, unknown_( Left, LUnknown ), select_n( LNotLightSize, HeavyAll, LNotLight, Heavy1 ), select_n( LNotHeavySize, LightAll, LNotHeavy, Light1 ), select_n( LUnknownSize, UnknownAll, LUnknown, Unknown1 ), Count is LNotLightSize + LNotHeavySize + LUnknownSize, Count >= 1, not_light( Right, RNotLight ), not_heavy( Right, RNotHeavy ), known_true( Right, RTrue ), unknown_( Right, RUnknown ), select_n( RNotLightSize, Heavy1, RNotLight, TableHeavy ), select_n( RNotHeavySize, Light1, RNotHeavy, TableLight ), select_n( RTrueSize, TrueAll, RTrue, TableTrue ), RUnknownSize is Count-(RNotLightSize+RNotHeavySize+RTrueSize), select_n( RUnknownSize, Unknown1, RUnknown, TableUnknown ), % Checksum to eliminate symmetrical solutions checksum( LNotHeavySize, LNotLightSize, LUnknownSize, 0, LeftChecksum ), checksum( RNotHeavySize, RNotLightSize, RUnknownSize, RTrueSize, RightChecksum ), LeftChecksum =< RightChecksum, not_light( Table, TableHeavy ), not_heavy( Table, TableLight ), known_true( Table, TableTrue ), unknown_( Table, TableUnknown ), length( TableHeavy, TableHeavySize ), length( TableLight, TableLightSize ), length( TableTrue, TableTrueSize ), length( TableUnknown, TableUnknownSize ), sum( Sizes, TotalSize ), information_content( Sizes, TotalSize, Content ). % A 'checksum' is used to ensure that only one member of each pair of % symmetrical solutions can be generated. checksum( LightSize, HeavySize, UnknownSize, TrueSize, Checksum ) :- Checksum is LightSize+(7*HeavySize)+(43*UnknownSize)+(259*TrueSize). % balance( +Left, +Right, +Counterfeit, ? Result ) holds when Result simulates % the outcome of testing the coin collections Left and Right with a balance, % given that 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, > ). % contains_coin( ?Collection, ?Coin ) holds when Coin is a member of % Collection. contains_coin( Collection, Coin ) :- part_collection( 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 unknown ordsets % comprising Collection. collection_to_set( Collection, Set ) :- known_true( Collection, KnownTrue ), not_heavy( Collection, NotHeavy ), not_light( Collection, NotLight ), unknown_( Collection, Unknown ), ord_union( [KnownTrue,NotHeavy,NotLight,Unknown], Set ). % inference( +CollectionA, ?CollectionB ) holds when (part) CollectionB comprises % the same coins as (part) CollectionA. inference( CollectionA, CollectionB ) :- unfolded( CollectionA, Coins ), unfolded( CollectionB, Coins ). % unfolded( +Collection, ?Coins ) holds when (part) Collection comprises Coins. unfolded( not_light(Collection), Coins ) :- not_light( Collection, Coins ). unfolded( not_heavy(Collection), Coins ) :- not_heavy( Collection, Coins ). unfolded( known_true(Collection), Coins ) :- known_true( Collection, Coins ). unfolded( unknown(Collection), Coins ) :- unknown_( 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 represents 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_collection( Left ), " on the left-hand pan", newline, tab( N ), "Put ", literal_collection( Right ), " on the right-hand pan", newline, tab( N ), "Leaving ", literal_collection( 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_collection( Collection ) --> {collection_to_set( Collection , [H|T] )}, literal_collection1( T, H ). literal_collection1( [], Number ) --> "the coin numbered ", literal( Number ). literal_collection1( [H|T], Number ) --> "the coins numbered ", literal( Number ), literal_collection2( T, H ). literal_collection2( [], Number ) --> " and ", literal( Number ). literal_collection2( [H|T], Number ) --> ", ", literal( Number ), literal_collection2( T, H ). 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". tab( 0 ) --> "". tab( s(N) ) --> " ", tab( N ). newline --> " ". % General Utility Predicates :- use_module( library(ordsets), [ord_union/2,ord_union/3] ), use_module( library(math), [log/2] ). information_content( Sizes, TotalSize, Content ) :- information_content1( Sizes, TotalSize, 0, Content ). information_content1( [], _TotalSize, Content, Content ). information_content1( [Size|Sizes], TotalSize, Content0, Content ):- ( Size > 0 -> Fraction is Size/TotalSize, log( Fraction, Log ), Content1 is Content0 + (Fraction * Log) ; otherwise -> Content1 = Content0 ), information_content1( Sizes, TotalSize, Content1, Content ). 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 ). :- ensure_loaded( puzzles(misc) ).