ASP Clingo - получение точного количества атомов

Question

Я с нетерпением жду возможности назначить определенное количество людей на определенную смену. Например, у меня шесть человек и три разные смены. Теперь я должен назначать на каждую смену ровно по два человека. Я пробовал что-то вроде этого, но...
ПРИМЕЧАНИЕ: это не сработает, поэтому, пожалуйста, редактируйте как можно быстрее, чтобы ввести людей в заблуждение, я даже удалил "." после этого никто не копирует:

person(a)
person(b)
person(c)
person(d)
person(e)
person(f)

shift("mor")
shift("aft")
shift("nig")

shiftCount(2).

{ assign(P,S) : shift(S)} = 1 :- person(P).

% DO NOT COPY THIS! SEE RIGHT ANSWER DOWN BELOW
:- #count{P : assign(P,"mor")} = K, shiftCount(K).
:- #count{P : assign(P,"aft")} = K, shiftCount(K).
:- #count{P : assign(P,"nig")} = K, shiftCount(K).


#show assign/2.

Можно ли подсчитать количество назначенных смен, чтобы я мог назначить столько людей, сколько задано?

Результатом приведенного выше кода (когда вставлен ".") Будет:

clingo version 5.5.0
Reading from stdin
Solving...
Answer: 1
assign(a,"nig") assign(b,"aft") assign(c,"mor") assign(d,"mor")
assign(e,"mor") assign(f,"mor")
SATISFIABLE

Models       : 1+
Calls        : 1
Time         : 0.021s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

Здесь вы с уверенностью можете увидеть, что утренняя ("морская") смена используется более двух раз, как указано в shiftCount. Что мне нужно изменить, чтобы получить желаемый результат?

Answer 1

Замените ваши 3-строчные ограничения на

{assign(P,S): person(P)} == K :- shift(S), shiftCount(K).

или, альтернативно, если вы хотите использовать запись ограничения:

:- {assign(P,S): person(P)} != K, shift(S), shiftCount(K).

В первой строке указано: для данного shiftCount K и за каждую смену S: количество назначений по всем людям P для этой смены S является K.
Ограничение гласит: это не может быть в случае shiftCount. K и смена S что количество назначений по всем людям P в смену S не является K.

Пожалуйста, не меняйте резко свой вопрос / образец кода, поскольку это может привести к тому, что этот ответ больше не будет работать.