SWI-Prolog et contraintes, bibliothèque CLP (FD)

Question

Je joue avec des contraintes dans (swi) prolog en utilisant la bibliothèque clpfd. J'essaie d'identifier quand un ensemble de contraintes encapsule ou subsume l'autre, p. Ex. X < 4 encapsule X < 7 à chaque fois que le premier est vrai, le second est vrai. Ceci peut être facilement représenté en utilisant l'implication logique. Cependant, je n'ai pas pu obtenir l'opérateur # ==> pour me donner le résultat que je voulais, donc j'ai recouru à l'utilisation de not (Co1 #/\ # \ Co2) où Co1 et Co2 sont des contraintes. C'est bien pour les contraintes individuelles, mais j'ai alors voulu passer une conjonctions de contraintes dans Co1 et Co2.

Maintenant, voici le frotter. Lorsque je tente

X#<7 #/\ #\X#<4. 

Je reviens

X in 4..6, 
X+1#=_G822, 
X+1#=_G834, 
_G822 in 5..7, 
_G834 in 5..7. 

(assez curieusement, ce faisant dans les résultats SICStus dans une erreur de segmentation)

Quand je passe dans

X#<7,X#<4 

I obtenir le

X in inf..3. 

Évidemment, je ne peux pas passer ce dernier en not (Co1 #/\ # \ Co2), mais le premier ne me donne pas le résultat que je veux. Quelqu'un peut-il expliquer pourquoi les deux approches donnent des résultats différents, et comment je peux faire en sorte que le premier agisse comme le second?

Answer 1

Il semble que vous ayez affaire à CLP (FD). Ces solveurs distinguent la phase d'installation et la phase d'étiquetage de la résolution d'un problème de contrainte.

Un solveur CLP (FD) ne réduit pas complètement un problème pendant la phase d'installation. Comme il a la possibilité de réduire les gammes variables pendant la phase d'étiquetage. Ainsi, il se peut que lors de la configuration, un problème soit posé par les autres solveurs à "Non", mais pas avec un solveur CLP (FD). Seulement pendant l'étiquetage, un "Non" sera détecté.

La quantité de réduction effectuée pendant la phase de configuration dépend fortement du système CLP (FD) donné. Certains systèmes CLP (FD) font plus de réduction pendant la phase d'installation, tandis que d'autres font moins. GNU Prolog utilise par exemple une propagation indexique, contrairement à SWI Prolog.Ainsi, nous trouvons par exemple, pas votre exemple:

SWI-Prolog:

?- X #< Y, Y #< Z, Z #< X. 
Z#=<X+ -1, 
X#=<Y+ -1, 
Y#=<Z+ -1. 

GNU Prolog:

?- X #< Y, Y #< Z, Z #< X. 
(7842 ms) no 

En outre, puisque vous utilisez des contraintes réifiées cela dépend aussi un peu comment intelligent la réification est terminée. Mais je suppose que dans le cas présent, c'est seulement une question de propagation. Nous trouvons maintenant votre exemple:

SWI-Prolog:

?- X #< 4 #==> X #< 7. 
X+1#=_G1330, 
X+1#=_G1342, 
7#>=_G1330#<==>_G1354, 
_G1354 in 0..1, 
_G1377#==>_G1354, 
_G1377 in 0..1, 
4#>=_G1342#<==>_G1377. 

GNU Prolog:

?- X #< 4 #==> X #< 7. 
X = _#22(0..268435455) 

Il y a un compromis entre faire plus de réduction dans la phase d'installation et de laisser plus de travail à la phase d'étiquetage. Et toute l'affaire dépend aussi de l'exemple donné. Mais quand vous avez aussi l'étiquetage à côté de la configuration, vous ne verrez aucune différence en termes de résultats:

SWI-Prolog:

?- X in 0..9, X #< 4 #==> X #< 7, label([X]). 
X = 0 ; 
X = 1 ; 
X = 2 ; 
X = 3 ; 
X = 4 ; 
X = 5 ; 
X = 6 ; 
X = 7 ; 
X = 8 ; 
X = 9. 

GNU Prolog:

?- fd_domain(X,0,9), X #< 4 #==> X #< 7, fd_labeling([X]). 
X = 0 ? ; 
X = 1 ? ; 
X = 2 ? ; 
X = 3 ? ; 
X = 4 ? ; 
X = 5 ? ; 
X = 6 ? ; 
X = 7 ? ; 
X = 8 ? ; 
X = 9 

Je n'ai pas testé avec SICStus Prolog ou B-Prolog. Mais je suppose qu'ils vont se comporter quelque part dans la vincité de SWI-Prolog et GNU Prolog. CLP (Q) n'est pas vraiment une alternative si votre domaine est vraiment FD, car il manquera certaines réductions "Non", que CLP (FD) ne manquerait pas. Par exemple ce qui suit est insatisfiable dans CLP (FD), mais satisfiable dans CLP (Q):

X = Y + 1, Y < Z, Z < X. 

Bye

Answer 2

La sous-contrainte des contraintes arithmétiques générales sur les entiers est indécidable en général, donc tous les solveurs corrects ont des limites inhérentes au-delà desquelles ils doivent retarder leurs réponses jusqu'à ce que l'on sache plus. Si vous savez que vos domaines sont finis, vous pouvez publier les domaines, puis essayer de trouver des contre-exemples qui rendraient l'implication invalide, en utilisant le prédicat marqueur/2 du solveur de contraintes. Considérons également que les inégalités linéaires sur Q sont décidables et que la bibliothèque de SWI-Prolog (clpq) est complète pour elles. Vous pouvez ainsi essayer vos contraintes CLP (Q) avec:

?- use_module(library(clpq)). 
true. 

?- { X < 4, X >= 7 }. 
false. 

et de voir qu'un tel existe dans Q contre-(donc pas non plus en Z), et donc l'implication détient.