Here’s a solution for 10 coins, using clpb:
main :-
between(1, 10, CF),
between(0, 1, HeavyInput),
once(main(CF, HeavyInput)),
fail.
main(CF, HeavyInput) :-
CoinCount = 10,
numlist(1, CoinCount, Is),
maplist(coin_i, Coins, Is),
maplist(coin_b, Coins, Bs),
sat(card([1], Bs)),
% Whether the 1 counterfeit coin is heavy or light, does not need to be determined
test_loop(Coins, input(CF, HeavyInput), Heavy, Steps),
length(Steps, StepsLen),
once(nth1(CFCalc, Bs, 1)),
format('Coin ~d with heavy ~d inputted - determined coin ~d with heavy ~k in ~d weighings\n', [CF, HeavyInput, CFCalc, Heavy, StepsLen]).
% Ends with the heavy side, then the light side
heavy_weigh(0, Side, Other, Side, Other).
heavy_weigh(1, Side, Other, Other, Side).
coin_i(c(I, _), I).
coin_b(c(_I, B), B).
certain_coin(c(_I, B)) :-
taut(B, _).
test_loop(Coins, Input, Heavy, Steps) :-
partition(certain_coin, Coins, Knowns, Us),
test_loop_(Us, Knowns, Coins, Input, Heavy, Steps).
% Don't care whether it's heavy or light
test_loop_([], _Knowns, _Coins, _Input, _Heavy, []).
test_loop_(Us, Knowns, Coins, Input, Heavy, Steps) :-
Us = [_|_],
% Choose some coins to weigh
once(prepare_weigh(Us, Knowns, Left, Right, UsExcl)),
maplist(coin_b, Left, LeftBs),
maplist(coin_b, Right, RightBs),
maplist(coin_b, UsExcl, UsExclBs),
weigh_coins(Input, side(Left, LeftBs), side(Right, RightBs), UsExclBs, Heavy),
Steps = [step(Left,Right)|Steps0],
test_loop(Coins, Input, Heavy, Steps0).
prepare_weigh([], _, [], [], []).
prepare_weigh([U1], [], [], [], [U1]).
prepare_weigh([U1], [K|_], [K], [U1], []).
% Need to vary the ordering, for maximum logical inferences, as explained at:
% http://www.murderousmaths.co.uk/books/12coinans.htm
% This particular varying is good enough for 10 coins, but can take 4 steps with 12 coins
prepare_weigh([U1,U2,U3], _Knowns, [U3], [U2], [U1]).
prepare_weigh([U1,U2], [], [U1], [U2], []).
prepare_weigh([U1,U2], [K|_], [U2], [K], [U1]).
prepare_weigh([U1,U2,U3|Us], Knowns, [U1|Left0], [U2|Right0], [U3|Excl0]) :-
prepare_weigh(Us, Knowns, Left0, Right0, Excl0).
weigh_coins(input(CF, HeavyInput), Left, Right, UsExcl, Heavy) :-
permutation([Left, Right], [Side1, Side2]),
Side1 = side(Coins, _),
memberchk(c(CF, _), Coins),
!,
% The excluded coins are all good
sat(card([0], UsExcl)),
% Map to the heavy side vs light side
heavy_weigh(HeavyInput, Side1, Side2, side(_, HeavyBs), side(_, LightBs)),
% clpb logic - 1 card is heavy xor 1 card is light
sat((card([1], HeavyBs) * Heavy) # (card([1], LightBs) * ~Heavy)).
weigh_coins(_Input, side(_, LeftBs), side(_, RightBs), _UsExcl, _Heavy) :-
% The weighed coins are all good
append(LeftBs, RightBs, Bs),
sat(card([0], Bs)).
Results:
?- main.
Coin 1 with heavy 0 inputted - determined coin 1 with heavy 1 in 3 weighings
Coin 1 with heavy 1 inputted - determined coin 1 with heavy 0 in 3 weighings
Coin 2 with heavy 0 inputted - determined coin 2 with heavy 1 in 3 weighings
Coin 2 with heavy 1 inputted - determined coin 2 with heavy 0 in 3 weighings
Coin 3 with heavy 0 inputted - determined coin 3 with heavy 1 in 3 weighings
Coin 3 with heavy 1 inputted - determined coin 3 with heavy 0 in 3 weighings
Coin 4 with heavy 0 inputted - determined coin 4 with heavy 1 in 3 weighings
Coin 4 with heavy 1 inputted - determined coin 4 with heavy 0 in 3 weighings
Coin 5 with heavy 0 inputted - determined coin 5 with heavy 1 in 3 weighings
Coin 5 with heavy 1 inputted - determined coin 5 with heavy 0 in 3 weighings
Coin 6 with heavy 0 inputted - determined coin 6 with heavy 1 in 3 weighings
Coin 6 with heavy 1 inputted - determined coin 6 with heavy 0 in 3 weighings
Coin 7 with heavy 0 inputted - determined coin 7 with heavy 1 in 3 weighings
Coin 7 with heavy 1 inputted - determined coin 7 with heavy 0 in 3 weighings
Coin 8 with heavy 0 inputted - determined coin 8 with heavy 1 in 3 weighings
Coin 8 with heavy 1 inputted - determined coin 8 with heavy 0 in 3 weighings
Coin 9 with heavy 0 inputted - determined coin 9 with heavy _ in 2 weighings
Coin 9 with heavy 1 inputted - determined coin 9 with heavy _ in 2 weighings
Coin 10 with heavy 0 inputted - determined coin 10 with heavy 1 in 3 weighings
Coin 10 with heavy 1 inputted - determined coin 10 with heavy 0 in 3 weighings
false.
Coin 9 gets determined quickly because it is the only coin excluded from the first 2 weighings, so it is inferred to be the counterfeit, but its heavy vs light weight is unknown because it has not been weighed at all.
I’m using a bit of a hack in prepare_weigh to vary the weighing sides. Perhaps sat_count/2 could be used to determine the optimum 2 sides to weigh.