Modeling symbolic puzzles

I have noticed that my unification over commutative monoid is almost exactly to solve a system of linear equations over the rational number domain as pointed by many others in this thread. Fortunately as I already wrote such a solver I feeded the puzzle to the solver:

% ?- solve_equations(a=b; 2*c=c+d; c=a+b; 2*c=e, X).

This is a general form of all solutions.

%@ X = ([d, c, b, a]=[0, 0, 0, 0]+e*[1r2, 1r2, 1r4, 1r4]) .

I borrowed the equations for the puzzle from @abeljue. Thanks.

% A=B
% 2C=C+D
% C=A+B
% 2C=E

I’ve read your thread just a few days ago, hence my late post. Here is my resolution:

equals(1, [1, c, 0, h, 0, s, 0, t, 0, r], [0, c, 1, h, 0, s, 0, t, 0, r]).
equals(2, [0, c, 0, h, 2, s, 0, t, 0, r], [0, c, 0, h, 1, s, 1, t, 0, r]).
equals(3, [0, c, 0, h, 1, s, 0, t, 0, r], [1, c, 1, h, 0, s, 0, t, 0, r]).
equals(4, [0, c, 0, h, 2, s, 0, t, 0, r], [0, c, 0, h, 0, s, 0, t, 1, r]).

% c/C = c/Circle, h/H = h/Hexagon, s/S = s/Square, t/T = t/Triangle, r/R
% = r/Rhombus

weight_shapes_possible(N, C, H, S, T, R) :-
    between(1, 16, C),
    between(1, 16, H),
    between(1, 16, S),
    between(1, 16, T),
    between(1, 16, R), % *
    equals(N, [C1, c, H1, h, S1, s, T1, t, R1, r], [C2, c, H2, h, S2, s, T2, t, R2, r]),
    A1 is C1 * C + H1 * H + S1 * S + T1 * T + R1 * R,
    A2 is C2 * C + H2 * H + S2 * S + T2 * T + R2 * R,
    A1 = A2.

% * If the most lightweight shape weighs 1, and, according to the
% picture, there are not more than two shapes of the same kind on one
% pile, the maximum weight of the least lightweight shape is 16, in case
% that one shape doubles the weight of the previous (1, 2, 4, 8, 16).

weight_shapes_certain(C, H, S, T, R) :-
    weight_shapes_possible(1, C, H, S, T, R),
    weight_shapes_possible(2, C, H, S, T, R),
    weight_shapes_possible(3, C, H, S, T, R),
    weight_shapes_possible(4, C, H, S, T, R),
    !.

in_balance([C1, c, H1, h, S1, s, T1, t, R1, r], [C2, c, H2, h, S2, s, T2, t, R2, r]) :-
    weight_shapes_certain(C, H, S, T, R),
    A1 is C1 * C + H1 * H + S1 * S + T1 * T + R1 * R,
    A2 is C2 * C + H2 * H + S2 * S + T2 * T + R2 * R,
    A1 = A2.

I don’t use CLP(FD). In the query you have to stick to the syntax of the in_balance predicate. Otherwise, I would have had to work with lists of different length and/or order, in which I am not very good at yet.

Perhaps you could omit one or two predicates, if you directly code the arithmetic conditions into the body of the weight_shapes_certain rule, but I wanted to start with a set of facts, not rules. Also, from a semantic perspective, the equals and in_balance predicates are practically identical, you could reformulate the latter as another instance of the former (after the other instances, and by adding ‘:- !’ to them), or vice versa. In my version the in_balance predicate just saves the first indexing argument of the equals predicate.

Better late than never: Here is my resolution, modified for use with two lists of different shape. It introduces four new clauses. Maybe a professional coder needs less, at the cost of readability. I also wrapped repetitive terms into higher-order predicates like maplist and foreach, in the last clause into a construction with bagof and permutation. That shortens the code - from a logical standpoint it’s just cosmetic.

equals(1, [1, c, 0, h, 0, s, 0, t, 0, r], [0, c, 1, h, 0, s, 0, t, 0, r]).
equals(2, [0, c, 0, h, 2, s, 0, t, 0, r], [0, c, 0, h, 1, s, 1, t, 0, r]).
equals(3, [0, c, 0, h, 1, s, 0, t, 0, r], [1, c, 1, h, 0, s, 0, t, 0, r]).
equals(4, [0, c, 0, h, 2, s, 0, t, 0, r], [0, c, 0, h, 0, s, 0, t, 1, r]).

% c/C = c/Circle, h/H = h/Hexagon, s/S = s/Square, t/T = t/Triangle, r/R
% = r/Rhombus

weight_shapes_possible(N, C, H, S, T, R) :-
    maplist(between(1, 16), [C, H, S, T, R]), % *
    equals(N, [C1, c, H1, h, S1, s, T1, t, R1, r], [C2, c, H2, h, S2, s, T2, t, R2, r]),
    A1 is C1 * C + H1 * H + S1 * S + T1 * T + R1 * R,
    A2 is C2 * C + H2 * H + S2 * S + T2 * T + R2 * R,
    A1 = A2.

% * If the most lightweight shape weighs 1, and, according to the
% picture, there are not more than two shapes of the same kind on one
% pile, the maximum weight of the least lightweight shape is 16, in case
% that one shape doubles the weight of the previous (1, 2, 4, 8, 16).

weight_shapes_certain(C, H, S, T, R) :-
    foreach(between(1, 4, N),
     weight_shapes_possible(N, C, H, S, T, R)),
    !.

valid_number_shape_pair(Number, Shape, List) :-
    member(Shape, [c, h, s, t, r]),
    bagof(Shape,
     member(Shape, List),
     Same_shape),
    length(Same_shape, 1),
    nth1(Position1, List, Number),
    nth1(Position2, List, Shape),
    succ(Position1, Position2),
    integer(Number),
    Number >= 0.

valid_list(List, All_pairs) :-
    bagof([Number, Shape],
     valid_number_shape_pair(Number, Shape, List),
     All_pairs),
    flatten(All_pairs, Permuted_list),
    permutation(Permuted_list, List),
    !.

number_of_same_shape(Number, Shape, List) :-
    valid_list(List, All_pairs),
    member([Number, Shape], All_pairs).

number_of_same_shape(0, Shape, List) :-
    valid_list(List, _),
    member(Shape, [c, h, s, t, r]),
    not(member(Shape, List)).

in_balance(List1, List2) :-
    weight_shapes_certain(C, H, S, T, R),
    bagof([Number1, Shape1],
     number_of_same_shape(Number1, Shape1, List1),
     Completed_pairs1),
    bagof([Number2, Shape2],
     number_of_same_shape(Number2, Shape2, List2),
     Completed_pairs2),
    permutation(Completed_pairs1, [[C1, c], [H1, h], [S1, s], [T1, t], [R1, r]]),
    permutation(Completed_pairs2, [[C2, c], [H2, h], [S2, s], [T2, t], [R2, r]]),
    A1 is C1 * C + H1 * H + S1 * S + T1 * T + R1 * R,
    A2 is C2 * C + H2 * H + S2 * S + T2 * T + R2 * R,
    A1 = A2,
    !.