Учитывая ваше описание предиката addUnique/2, для реализации решения можно использовать программирование логики ограничений. Это далеко от новичка, но я все равно выложу объяснение.
Во-первых, возможно, стоит поискать, что такое программирование логики ограничений и как использовать реализацию (например, SWI-PL clpfd ). По сути, программирование логики ограничений (в частности, решатель конечных областей) позволит вам указать следующие ограничения для ваших переменных в списке ввода на addUnique/2:
- Как переменные в вашем входном списке могут связываться с определенными числовыми значениями (т. Е. Целыми числами от 0 до и включая указанное значение)
- Как разные переменные в вашем входном списке не могут одновременно связываться с одним и тем же значением (т. Е.,! = Где разные)
- Как сумма переменных во входном списке плюс любые числа должны складываться до заданного значения (т. Е. Максимального значения, которое переменные могут принимать в 1, выше).
Вместе эти спецификации позволят основному решателю ограничений автоматически определять, какие допустимые значения могут одновременно принимать переменные с учетом указанных выше ограничений, предоставляя вам ваши решения (их может быть несколько, один или ни одного).
Вот решение с использованием вышеупомянутого решателя ограничений в SWI-PROLOG (решатель clpfd):
:- use_module(library(clpfd)). % import and use the constraint solver library
addUnique([A|As], Val) :-
unique_vars([A|As], UVs), % determine all unique variables
UVs ins 0..Val, % (1) domain of all unique variables is 0 to Val
pairwise_inequ(UVs), % (2) all unique variables are pairwise !=
construct_sum_constr(As, Val, A, Program), % (3) construct the sum constraint
Program, % assert the sum constraint
label(UVs). % label domains to enumerate a solution (backtracks)
% predicate to return a list of unique vars, if present
unique_vars([], []).
unique_vars([V|Vs], [V|Uniq]) :-
var(V),
\+ var_memberchk(V, Vs), !,
unique_vars(Vs, Uniq).
unique_vars([_|Vs], Uniq) :-
unique_vars(Vs, Uniq).
% predicate to test if a variable appears in a list (possibly including variables)
var_memberchk(V0, [V1|_]) :-
V0 == V1, !.
var_memberchk(V0, [_|V1s]) :-
var_memberchk(V0, V1s).
% create constraints that assert each in the input list != to each other
pairwise_inequ([]).
pairwise_inequ([V|Vs]) :-
map_inequ(Vs, V),
pairwise_inequ(Vs).
% predicate to pairwise assert inequality between all list members
map_inequ([], _).
map_inequ([V1|V1s], V0) :-
V0 #\= V1, % the inequality constraint
map_inequ(V1s, V0).
% predicate to construct a summation constraint, whereby all variables in the
% input list are constructed into a sum with +/2 and finally equated to a value
construct_sum_constr([], Val, Sum, (Sum #= Val)).
construct_sum_constr([V|Vs], Val, Sum, Program) :-
construct_sum_constr(Vs, Val, (V + Sum), Program).
Запуск этого кода, например, дает вам:
?- addUnique([A,B,B], 6).
A = 0,
B = 3 ;
A = 4,
B = 1 ;
A = 6,
B = 0.
; перечисляет следующее решение для допустимых привязок между переменными. Обратите внимание, что A и B никогда не принимают одно и то же значение, как требуется, но все вхождения в списке ввода всегда будут суммироваться до 6. Другой запрос:
?- addUnique([A,A,A],4).
false.
Результатом является сбой, поскольку не найдено ни одного целого числа, связывающего с A, которое при суммировании составило 4, тогда как:
?- addUnique([A,A,A,A],4).
A = 1.
... как и ожидалось. Также вы хотели попробовать:
?- addUnique([A,B,C,D],4).
false.
Опять же, результатом здесь является сбой, потому что все переменные A, B, C и D были утверждены как разные и не могут все связываться с 1.
РЕДАКТИРОВАТЬ пс. Они тоже хотели попробовать:
?- addUnique([A,A,A,1],4).
A = 1.
Простая модификация приведенного выше кода гарантирует, что при вызове ins для утверждения доменов используются только переменные (а не числа в списке ввода).