Os problemas de satisfação de restrições podem ser resolvidos com o Prolog?

O tipo de problemas com "presença na festa" pode ser solucionado no Prolog? Por exemplo:

Burdock Muldoon e Carlotta Pinkstone disseram que viriam se Albus Dumbledore viesse. Albus Dumbledore e Daisy Dodderidge disseram que viriam se Carlotta Pinkstone viesse. Albus Dumbledore, Burdock Muldoon e Carlotta Pinkstone disseram que viriam se Elfrida Clagg viesse. Carlotta Pinkstone e Daisy Dodderidge disseram que viriam se Falco Aesalon viesse. Burdock Muldoon, Elfrida Clagg e Falco Aesalon disseram que viriam se Carlotta Pinkstone e Daisy Dodderidge viessem. Daisy Dodderidge disse que viria se Albus Dumbledore e Burdock Muldoon viessem. A quem precisa ser persuadido a participar da festa para garantir que todos os seus convidados participem?

Eu tentei expressar isso no GNU Prolog:

attend(BM) :- attend(AD).
attend(CP) :- attend(AD).
attend(AD) :- attend(CP).
attend(DD) :- attend(CP). 
attend(AD) :- attend(EC).
attend(BM) :- attend(EC).
attend(CP) :- attend(EC). 
attend(CP) :- attend(FA).
attend(DD) :- attend(FA).
attend(BM) :- attend(CP),attend(DD).
attend(EC) :- attend(CP),attend(DD).
attend(FA) :- attend(CP),attend(DD).
attend(DD) :- attend(AD),attend(BM).

attend(FA). /* try different seed invitees in order to see if all would attend*/

/* input:
write('invited:'),nl,
  attend(X),write(X),nl,
  fail.*/

Estou com estouro de pilha (sem trocadilhos) e não tenho conhecimento de avaliação de prólogo, é por isso que estou perguntando.

De um modo geral, esse problema pode ser convertido na fórmula de satisfação CNF booleana (com 6 variáveis ​​booleanas). Portanto, a perspectiva do prólogo tem algum mérito?

Para resolver um problema com o Prolog, como em qualquer linguagem de programação, seja ela declarativa ou imperativa, é necessário pensar na representação da solução e da entrada.

Como essa é uma questão de programação, teria sido popular no StackOverflow.com, onde os programadores resolvem problemas de programação. Aqui eu tentaria ser mais científico.

$Attend(X) \to Attend(Y) \wedge Attend(Z)$$Attend(AD)\wedge Attend(BM)\to Attend(DD)$

Daisy Dodderidge disse que viria se Albus Dumbledore e Burdock Muldoon viessem

são mais difíceis de tratar.

Com o Prolog, a primeira abordagem simples é evitar uma reversão completa do relacionamento e, em vez disso, ser direcionada à meta.

Assuma uma ordem na lista de convidados e use uma regra

$\qquad \left\{\begin{align} A(X)\wedge A(Y) &\to A(Z), \\ A(W)&\to A(X), \\ A(W)&\to A(Y), \\ X&<Z, \\ Y&<Z\end{align}\right\}\quad \vdash \quad A(W) \to A(Z)$

$A(X)$$Attend(X)$

Esta regra é fácil de implementar.

Uma abordagem bastante ingênua

Para facilitar a leitura, followsseja a relação dada como entrada e bringsseja o seu inverso.

Então a entrada é dada por

follows(bm,[ad]).
follows(cp,[ad]).
follows(ad,[cp]).
follows(dd,[cp]).
follows(ad,[ec]).
follows(bm,[ec]).
follows(cp,[ec]).
follows(cp,[fa]).
follows(dd,[fa]).
follows(bm,[cp,dd]).
follows(ec,[cp,dd]).
follows(fa,[cp,dd]).
follows(dd,[ad,bm]).

E bringspode ser definido da seguinte maneira:

brings(X,S):-brings(X,S,[]).

brings(_X,[],_S).
brings(X,[X|L],S):-brings(X,L,[X|S]).
brings(X,[Y|L],S):-follows(Y,[X]),brings(X,L,[Y|S]).
brings(X,[Y|L],S):-follows(Y,[A,B]),
          member(A,S),member(B,S),brings(X,L,[Y|S]).

brings/3(X,L,S)$X$ comparecer.

Se definirmos

 partymaker(X):-Guests=[ad,bm,cp,dd,ec,fa],member(X,Guests),brings(X,Guests).

Temos as seguintes soluções exclusivas:

 [ad,ec]

Esta não é a lista completa, pois sob a ordem alfabética da cláusula

 follows(bm,[cp,dd]).

não está funcionando.

Uma solução bastante envolvida para o quebra-cabeça original

Para resolver o problema completamente, você deve realmente deixar o sistema tentar provar a presença de convidados posteriores sem introduzir loops infinitos na árvore de pesquisa. Existem várias maneiras de atingir esse objetivo. Cada um tem suas vantagens e desvantagens.

Uma maneira é redefinir da brings/2seguinte maneira:

brings(X,S):-brings(X,S,[],[]).

% brings(X,RemainsToBring,AlreadyTaken,AlreadyTried).
%
% Problem solved
brings(_X,[],_S,_N). 
% Self
brings(X,[X|L],S,N):-brings(X,L,[X|S],N). 
% Follower
brings(X,[Y|L],S,N):-follows(Y,[X]),brings(X,L,[Y|S],N). 
% Y is not a follower, but X can bring 2
brings(X,[Y|L],S,N):- \+member(Y,N),\+follows(Y,[X]), 
                   follows(Y,[A,B]),
                   try_bring(X,A,L,S,[Y|N]),
                   try_bring(X,B,L,S,[Y|N]),brings(X,L,[Y|S],N).
% Y is not a follower, but X can bring 1
brings(X,[Y|L],S,N):- \+member(Y,N),\+follows(Y,[X]),\+follows(Y,[_A,_B]), 
                   follows(Y,[C]),
                   try_bring(X,C,L,S,[Y|N]),brings(X,L,[Y|S],N).

try_bring(_X,A,_L,S,_N):-member(A,S).
try_bring(X,A,L,S,N):- \+member(A,S),sort([A|L],Y),brings(X,Y,S,N).

O último argumento em brings/4 é necessário para evitar um loop infinito try_bring.

Isso fornece as seguintes respostas: Albus, Carlotta, Elfrida e Falco. No entanto, essa solução não é a mais eficiente, uma vez que o retorno é introduzido, onde às vezes pode ser evitado.

Uma solução geral

$r(X,S): V \to V'$

$S \subseteq V$$V' = V \cup \{X\}$

$V$$U$$V$

add_element(X,V,U):- ( var(V) -> % set difference that works in both modes
                           member(X,U),subtract(U,[X],V);
                      \+member(X,V),sort([X|V],U) ).

support(V,U):- guests(G), % rule application
               member(X,G),
               add_element(X,V,U),
               follows(X,S),
               subset(S,V).

set_support(U,V):- support(V1,U), % sort of a minimal set
               ( support(_V2,V1) -> 
                      set_support(V1,V) ; 
                 V = V1). 

is_duplicate(X,[Y|L]):- ( subset(Y,X) ; is_duplicate(X,L) ).

% purging solutions that are not truly minimal
minimal_support(U,L):-minimal_support(U,[],L).
minimal_support([],L,L).
minimal_support([X|L],L1,L2):-( append(L,L1,U),is_duplicate(X,U) -> 
                                    minimal_support(L,L1,L2); 
                                minimal_support(L,[X|L1],L2) ).


solution(L):- guests(G),setof(X,set_support(G,X),S),
              minimal_support(S,L).

Agora, se, por exemplo, o conjunto de dados # 2 for fornecido como

follows(fa,[dd,ec]).
follows(cp,[ad,bm]).
guests([ad,bm,cp,dd,ec,fa]).

Nós obtemos a resposta L = [[ad, bm, dd, ec]]. O que significa que todos os convidados, exceto Carlotte e Falco, devem ser convidados.

As respostas que essa solução me deu correspondem às soluções fornecidas no artigo da Wicked Witch, com exceção do conjunto de dados # 6, onde mais soluções foram produzidas. Esta parece ser a solução correta.

Finalmente, devo mencionar a biblioteca de Prolog CLP (FD) que é particularmente adequada para esse tipo de problemas.

Como observado por svick, o primeiro problema com o código no OP é que nomes começando com letras maiúsculas são variáveis ​​no Prolog. Portanto, admit(CP) :- admit(AD)é equivalente a attend(X) :- attend(Y), o que resulta no Prolog entrando imediatamente em um loop infinito, tentando demonstrar que attendé válido por algum termo, encontrando algum termo para o qual attendé válido.

No entanto, se você quisesse que cada conjunto de iniciais fosse um termo distinto concreto, ainda ocorreria um estouro de pilha porque você tem ciclos, por exemplo

attend(cp) :- attend(ad).
attend(ad) :- attend(cp).

Portanto, para descobrir se há attend(cp)retenções, o Prolog tentará determinar se há attend(ad)retenções, o que será feito verificando seattend(cp) retenções e assim por diante até o estouro da pilha.

Não acredito que o baunilha Prolog faça qualquer tentativa de determinar se existe esse ciclo e examine outras maneiras de fazer uma delas attend(cp)ou attend(ad)verdadeira, em vez de ficar preso em um loop infinito.

Pode ou não haver versões do Prolog compatíveis com esse recurso. Eu estou mais familiarizado com Mercury e acho que a "apresentação mínima do modelo" de Mercury é exatamente o que você precisa para este caso. Na verdade, nunca o usei, mas meu entendimento é que mais ou menos permite que um termo que se implique seja considerado verdadeiro se houver alguma outra maneira de provar isso, ou falso caso contrário, sem ser pego em um loop infinito. Consulte a seção relevante dos documentos Mercury e, se você estiver interessado, um documento descrevendo a implementação.

O Mercury é uma linguagem de programação lógica de pureza forçada, com sintaxe semelhante ao Prolog, mas sistemas fortes de tipo e modo, e é compilada em vez de interpretada.

Acabei de repensar a introdução do artigo (que não leio há algum tempo), e ele menciona que o tabling foi implementado em várias versões do Prologs, para que você possa ir mais longe pesquisando no Google. em Prolog.

Encontrei o seguinte artigo sobre resolução de SAT usando o prólogo:

• Uma pérola na resolução de SAT em Prolog por Jacob M. Howe e Andy King

Uma implementação do solucionador pode ser encontrada aqui .

Veja esta resposta do stackoverflow para obter detalhes sobre o código e como usá-lo.

Deixando de lado a questão minúscula / maiúscula, há um ciclo nas cláusulas:

attend(cp) :- attend(ad).
attend(ad) :- attend(cp).

Portanto, quando você chama um intérprete de cima para baixo, ele faz um loop. Você pode ter mais sorte com a Programação de conjunto de respostas (ASP), que funciona de baixo para cima. Aqui está uma codificação via biblioteca ( minimal / asp ):

:- use_module(library(minimal/asp)).

choose([admit(bm)]) <= posted(admit(ad)).
choose([admit(cp)]) <= posted(admit(ad)).
choose([admit(ad)]) <= posted(admit(cp)).
choose([admit(dd)]) <= posted(admit(cp)).
choose([admit(ad)]) <= posted(admit(ec)).
choose([admit(bm)]) <= posted(admit(ec)).
choose([admit(cp)]) <= posted(admit(ec)).
choose([admit(cp)]) <= posted(admit(fa)).
choose([admit(dd)]) <= posted(admit(fa)).
choose([admit(bm)]) <= posted(admit(cp)),posted(admit(dd)).
choose([admit(ec)]) <= posted(admit(cp)),posted(admit(dd)).
choose([admit(fa)]) <= posted(admit(cp)),posted(admit(dd)).
choose([admit(dd)]) <= posted(admit(ad)),posted(admit(bm)).

choose([admit(fa)]) <= posted(init).

Aqui está um exemplo de execução:

Jekejeke Prolog 3, Runtime Library 1.3.8 (23 May 2019)

?- post(init), listing(admit/1).
admit(fa).
admit(cp).
admit(ad).
admit(bm).
admit(dd).
admit(ec).