Les problèmes de satisfaction des contraintes peuvent-ils être résolus avec Prolog?

Est-ce que les problèmes de type "fréquentation des partis" sont résolus dans Prolog? Par exemple:

Burdock Muldoon et Carlotta Pinkstone ont tous deux déclaré qu'ils viendraient si Albus Dumbledore venait. Albus Dumbledore et Daisy Dodderidge ont tous deux déclaré qu'ils viendraient si Carlotta Pinkstone venait. Albus Dumbledore, Burdock Muldoon et Carlotta Pinkstone ont tous dit qu'ils viendraient si Elfrida Clagg venait. Carlotta Pinkstone et Daisy Dodderidge ont toutes deux déclaré qu'elles viendraient si Falco Aesalon venait. Burdock Muldoon, Elfrida Clagg et Falco Aesalon ont tous dit qu'ils viendraient si Carlotta Pinkstone et Daisy Dodderidge venaient tous les deux. Daisy Dodderidge a dit qu'elle viendrait si Albus Dumbledore et Burdock Muldoon venaient tous les deux. Qui doit être persuadé d'assister à la fête afin de s'assurer que tous ses invités y assistent?

J'ai essayé d'exprimer cela dans 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.*/

Je rencontre un débordement de pile (sans jeu de mots) et je n'ai aucune connaissance de l'évaluation de prologue, c'est pourquoi je demande.

De manière générale, ce problème peut être transposé dans la formule de satisfaction booléenne CNF (avec 6 variables booléennes). Par conséquent, la perspective prologue est-elle valable?

Pour résoudre un problème avec Prolog, comme avec tout langage de programmation, qu'il soit déclaratif ou impératif, vous devez penser à la représentation de la solution et de l'entrée.

Comme il s'agit d'une question de programmation, elle aurait été populaire sur StackOverflow.com où les programmeurs résolvent les problèmes de programmation. Ici, j'essaierais d'être plus scientifique.

Pour résoudre le problème dans l'OP, il faut inverser la relation définie par les dépendances indiquées dans l'entrée. Les clauses de la forme sont faciles à inverser. Les clauses A t t e n d ( A D ) ∧ A t t e n d $Attend(X) \to Attend(Y) \wedge Attend(Z)$ comme$Attend(AD)\wedge Attend(BM)\to Attend(DD)$

Daisy Dodderidge a dit qu'elle viendrait si Albus Dumbledore et Burdock Muldoon venaient tous les deux

sont plus difficiles à traiter.

Avec Prolog, la première approche simple consiste à éviter un renversement complet de la relation et à être plutôt orienté vers un objectif.

Supposons une commande sur la liste des invités et utilisez une règle

$\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)$

(Nous utilisons au lieu de A t t e n d ( X ) pour faire court)$A(X)$$Attend(X)$

Cette règle est facile à mettre en œuvre.

Une approche plutôt naïve

Pour la lisibilité, followssoit la relation donnée en entrée, et bringsson inverse.

Ensuite, l'entrée est donnée par

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]).

Et bringspeut être défini comme suit:

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$

Si nous définissons

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

Nous obtenons les solutions uniques suivantes:

 [ad,ec]

Ce n'est pas la liste complète, car dans l'ordre alphabétique, la clause

 follows(bm,[cp,dd]).

ne fonctionne pas.

Une solution plutôt impliquée au puzzle original

Pour résoudre complètement le problème, vous devez laisser le système essayer de prouver la présence des invités ultérieurs sans introduire de boucles infinies dans l'arborescence de recherche. Il existe plusieurs façons d'atteindre cet objectif. Chacun a ses avantages et désavantages.

Une façon consiste à redéfinir brings/2comme suit:

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).

Le dernier argument dans brings/4est nécessaire pour éviter une boucle infinie try_bring.

Cela donne les réponses suivantes: Albus, Carlotta, Elfrida et Falco. Cependant, cette solution n'est pas la plus efficace car le retour en arrière est introduit là où il est parfois possible de l'éviter.

Une solution générale

$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).

Maintenant, si par exemple l'ensemble de données # 2 est donné comme

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

Nous obtenons la réponse L = [[ad, bm, dd, ec]]. Ce qui signifie que tous les invités sauf Carlotte et Falco doivent être invités.

Les réponses que cette solution m'a données correspondaient aux solutions données dans l'article Wicked Witch à l'exception du jeu de données # 6, où plus de solutions ont été produites. Cela semble être la bonne solution.

Enfin, je dois mentionner la bibliothèque CLP (FD) de Prolog qui est particulièrement adaptée à ce type de problèmes.

Comme repéré par svick, le premier problème avec le code dans l'OP est que les noms commençant par des lettres majuscules sont des variables dans Prolog. Donc, admit(CP) :- admit(AD)est équivalent à attend(X) :- attend(Y), ce qui fait que Prolog entre immédiatement dans une boucle infinie essayant de démontrer que attendtient pour un terme en trouvant un terme pour lequel attendtient.

Cependant, si vous vouliez que chaque ensemble d'initiales soit un terme distinct concret, vous rencontrerez toujours un débordement de pile car vous avez des cycles, par exemple

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

Donc, pour savoir si les attend(cp)suspensions, Prolog essaiera de déterminer si les attend(ad)suspensions, ce qu'il fera en vérifiant si les attend(cp)suspensions, et ainsi de suite jusqu'au débordement de la pile.

Je ne crois pas que vanilla Prolog tente de déterminer s'il existe un tel cycle et d'examiner d' autres façons de faire l'un attend(cp)ou le attend(ad)vrai plutôt que de rester coincé dans une boucle infinie.

Il peut y avoir ou non des versions de Prolog qui prennent en charge une telle fonctionnalité. Je connais mieux Mercury et je pense que le "dépôt de modèle minimal" de Mercury est exactement ce dont vous avez besoin pour cette affaire. Je ne l'ai jamais réellement utilisé, mais d'après ce que je comprends, il permet plus ou moins à un terme qui implique lui-même d'être considéré comme vrai s'il existe un autre moyen de le prouver, ou faux sinon, sans se faire prendre dans une boucle infinie. Consultez la section pertinente de la documentation Mercury et, si vous êtes intéressé, un article décrivant la mise en œuvre.

Mercury est un langage de programmation logique de pureté forcée, avec une syntaxe similaire à Prolog mais des systèmes de type et de mode forts, et il est compilé plutôt qu'interprété.

Je viens de recréer l'introduction du document (que je n'ai pas lu depuis un certain temps), et il mentionne que le dépôt a été implémenté dans plusieurs versions de Prologs, il se peut donc que vous puissiez aller plus loin en recherchant le dépôt sur Google dans Prolog.

J'ai trouvé l'article suivant sur la résolution SAT à l'aide de prolog:

• A Pearl on SAT Solving in Prolog par Jacob M. Howe et Andy King

Une implémentation du solveur peut être trouvée ici .

Voir cette réponse stackoverflow pour plus de détails sur le code et comment l'utiliser.

Mis à part le problème des minuscules / majuscules, il y a un cycle dans les clauses:

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

Ainsi, lorsque vous appelez un interprète descendant, il se met en boucle. Vous aurez peut-être plus de chance avec la programmation par ensemble de réponses (ASP), qui fonctionne de bas en haut. Voici un codage via la bibliothèque ( 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).

Voici un exemple d'exécution:

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).