The Counterfeit Coin Puzzle

go 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 ).

coins( [1,2,3,4,5,6,7,8,9,10,11,12] ).

counterfeit_weight( heavy ).
counterfeit_weight( light ).

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';
• 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 is defined by its number, and whether it is heavy or light.

counterfeit( counterfeit(Coin, HeavyOrLight), Coin, HeavyOrLight ).

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 × 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 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, Right 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.

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

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

:-  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 ).

Load a small library of puzzle utilities.

:- ensure_loaded( misc ).