<div class="notebook">

<div class="nb-cell markdown" name="md1">
A man has 10 nickels among which there is a single counterfeit coin, which is either heavier or lighter than the other ones.

How can one tell in weightings whether there is a counterfeit nickel, and if so which one it is?
</div>

<div class="nb-cell markdown" name="md2">
You are given a set of scales and 12 marbles. The scales are of the old balance variety. That is, a small dish hangs from each end of a rod that is balanced in the middle. The device enables you to conclude either that the contents of the dishes weigh the same or that the dish that falls lower has heavier contents than the other.

The 12 marbles appear to be identical. In fact, 11 of them are identical, and one is of a different weight. Your task is to identify the unusual marble and discard it. You are allowed to use the scales three times if you wish, but no more.

Note that the unusual marble may be heavier or lighter than the others. You are asked to both identify it and determine whether it is heavy or light. 
</div>

<div class="nb-cell markdown" name="md3">
See https://puzzles.nigelcoldwell.co.uk/one.htm and the email answer for a better explanation of this solution.

We will use clpfd to solve this problem
</div>

<div class="nb-cell program" data-background="true" name="p1">
:- use_module(library(clpfd)).
:- use_rendering(table).
:- op(920,fy, *).

*_.
</div>

<div class="nb-cell program" data-background="true" name="p2">
marbles(N, Marbles) :-
    length(Marbles, N),
    N1 #= N - 1,
    tuples_in([[N2, N3]], [[0, 1], [1, 0]]),
    global_cardinality(Marbles, [1-N1, 0-N2, 2-N3]).
</div>

<div class="nb-cell query" name="q1">
marbles(12, Marbles), label(Marbles).
</div>

<div class="nb-cell markdown" name="md4">
The basic idea of the number theory solution is that you can encode a ternary number from the results of the weighings and relate that ternary number to the index of the marble and its weight.

So let's say that:

* if the left side goes up, it's -1
* if both side stays equal, it's 0
* if the right side goes up, it's 1
</div>

<div class="nb-cell program" data-background="true" name="p3">
ternary_decimal(Digits, Ternary, Decimal) :-
    length(Ternary, Digits),
    Ternary ins -1..1,
    N1 #= Digits - 1,
    length(Coeffs, Digits),
    numlist(0, N1, Powers),
   	maplist([X, Y]&gt;&gt;(Y #= 3^X), Powers, Coeffs),
    scalar_product(Coeffs, Ternary, #=, Decimal).

triples(Digits, Triples) :-
    N #= (3^Digits - 3) // 2,
    numlist(1, N, PositiveDecimals),
    length(PositiveTriples, N),
    maplist(ternary_decimal(Digits), PositiveTriples, PositiveDecimals),
	maplist([X, Y]&gt;&gt;(Y #= -X), PositiveDecimals, NegativeDecimals),
    length(NegativeTriples, N),
    maplist(ternary_decimal(Digits), NegativeTriples, NegativeDecimals),
    transpose([NegativeTriples, PositiveTriples], Triples).
</div>

<div class="nb-cell query" name="q2">
triples(3, Triples).
</div>

<div class="nb-cell markdown" name="md5">
Now, the crucial part is to find a combination of triples which will map a single ternary number to a single marble.

For this, you need to choose N triples, one of each mirrored triples so that the columns (or weighing) has the same number of marbles on each side. This means that the sum of a column should equal to 0.
</div>

<div class="nb-cell program" data-background="true" name="p4">
choose_triples(N, Digits, AllTriples, LeftRight, ChosenDecimals) :-
    length(SubTriples, N),
    subseq(AllTriples, SubTriples, _),
    length(ChosenTriples, N),
    maplist({Digits}/[L]&gt;&gt;(length(L, Digits)), ChosenTriples),
    maplist([V, T]&gt;&gt;(tuples_in([V], T)), ChosenTriples, SubTriples),
    transpose(ChosenTriples, Columns),
    maplist([C]&gt;&gt;(sum(C, #=, 0)), Columns),
    append(ChosenTriples, Vars),
    label(Vars),
    % the rest of the code is just a reformating of ChosenTriples to work with indices
    maplist(ternary_decimal(3), ChosenTriples, ChosenDecimals),
   	length(Indices, Digits),
    maplist(numlist(1, N), Indices),
    length(Pairs, Digits),
    maplist(pairs_keys_values, Pairs, Columns, Indices),
    maplist(keysort, Pairs, SortedPairs),
    maplist(group_pairs_by_key, SortedPairs, GroupedPairs),
    maplist([[-1-Left, _, 1-Right], [Left, Right]]&gt;&gt;(true), GroupedPairs, LeftRight).
</div>

<div class="nb-cell query" name="q3">
Digits = 3, triples(Digits, Triples), choose_triples(10, Digits, Triples, Groupings, Decimals).
</div>

<div class="nb-cell markdown" name="md6">
In order to find the different marble or coin, we just need to do the different weighing, convert the weighing result from its ternary representation to decimal and find if it is in the lighter set or heavier set. The index of that decimal number is the index of the marble.
</div>

<div class="nb-cell program" data-background="true" name="p5">
weigh(List, Groupings, Order) :-
    maplist(maplist({List}/[I, E]&gt;&gt;(nth1(I, List, E))), Groupings, [Left, Right]),
    sum(Left, #=, LeftSum),
    sum(Right, #=, RightSum),
    Diff #= LeftSum - RightSum,
    % below is just zcompare but with -1, 0 and 1
    Order in -1..1,
    Diff #&lt; 0 #&lt;==&gt; Order #= -1,
    Diff #= 0 #&lt;==&gt; Order #= 0,
    Diff #&gt; 0 #&lt;==&gt; Order #= 1.

weight(LoneDecimal, Weight, Decimal) :-
    % Weight = 0 means it is lighter, Weight = 1 means it is heavier
    Decimal #= LoneDecimal #==&gt; Weight #= 0,
    Decimal #= -LoneDecimal #==&gt; Weight #= 1.

find_lone(Digit, Marbles, Groupings, Decimals, Decimal, LoneIndex, Lone, Weight) :-
    maplist(weigh(Marbles), Groupings, Orders),
    ternary_decimal(Digit, Orders, Decimal),
	maplist(weight(Decimal, Weight), Decimals),
    DecimalValue #= Weight * -1 * Decimal + (1 - Weight) * Decimal,
    element(LoneIndex, Decimals, DecimalValue),
    element(LoneIndex, Marbles, Lone).
</div>

<div class="nb-cell query" name="q4">
Digit = 3, N = 10,
triples(Digit, Triples), choose_triples(N, Digit, Triples, Groupings, Decimals),
marbles(N, Marbles),
label(Marbles),
find_lone(Digit, Marbles, Groupings, Decimals, LoneDecimal, LoneIndex, Lone, Weight).
</div>

</div>