prolog - rae - sobretodo junto o separado

¿Reificación obligatoria cuando se usa el operador ''mod'' junto con ''o''?

Question

He escrito un programa CSP usando CLP (FD) y SWI-Prolog.

Creo que necesito mejorar la escritura de mis restricciones cuando utilizo el operador de mod junto con #// en mis predicados.

Un pequeño ejemplo:

:- use_module(library(clpfd)).
constr(X,Y,Z) :-
X in {1,2,3,4,5,6,7},
Y in {3,5,7},
Z in {1,2},
((X #= 3)) #==> ((Y mod 3 #= 0) #// (Y mod 7 #= 0)),
((Z #= 1)) #<==> ((Y mod 3 #= 0) #// (Y mod 7 #= 0)).

Si llamo constr(3,Y,Z). , Obtengo Z #= 1 o Z #= 2 . Esto se debe a que algunas variables intermedias (relativas a las expresiones mod ) aún deben ser evaluadas.

Por supuesto, lo ideal sería obtener solo Z #= 1 .

Como se puede hacer esto ?

Sé que si escribo en su lugar

((X #= 3)) #==> ((Z #= 1)),
((Z #= 1)) #<==> ((Y mod 3 #= 0) #// (Y mod 7 #= 0)).

todo funciona como se espera

¿Pero esta reificación es obligatoria? Quiero decir, ¿tengo que crear una variable de reificación cada vez que tengo este patrón en mis restricciones?

(A mod n1 #= 0) #// (B mod n2 #= 0) #// ... #// (Z mod n26 #= 0)

Gracias de antemano por tus ideas.

Answer 1

¡Esa es una muy buena observación y pregunta! Primero, tenga en cuenta que esto no es de ninguna manera específico para mod/2 . Por ejemplo:

?- B #<==> X #= Y+Z, X #= Y+Z. B in 0..1, X#=_G1122#<==>B, Y+Z#=X, Y+Z#=_G1122.

Por el contrario, si escribimos esto declarativamente de manera equivalente como:

?- B #<==> X #= A, A #= Y + Z, X #= A.

entonces obtenemos exactamente como esperábamos

A = X, B = 1, Y+Z#=X.

¿Que esta pasando aqui? En todos los sistemas que conozco, la reificación en general usa una descomposición de expresiones CLP (FD) que desafortunadamente elimina información importante que no se recupera más tarde. En el primer ejemplo, no se detecta que la restricción X #= Y+Z esté implicada , es decir, se mantenga necesariamente .

Por otro lado, la vinculación de una única igualdad con argumentos no compuestos se detecta correctamente, como en el segundo ejemplo.

Entonces, sí, en general, necesitará reescribir sus restricciones de esta manera para permitir la detección óptima de vinculación.

La pregunta que acecha es, por supuesto, si el sistema CLP (FD) podría ayudarlo a detectar dichos casos y realizar la reescritura automáticamente . También en este caso, la respuesta es sí , al menos para ciertos casos. Sin embargo, al sistema CLP (FD) normalmente solo se le indican restricciones individuales en una secuencia determinada, y la recreación y el análisis de una visión general global de todas las restricciones publicadas para fusionar o combinar las restricciones descompuestas previamente no suele valer la pena.

Answer 2

Con el predicado contracting/1 (semioficial), puede minimizar algunos dominios de una sola vez. En tu caso:

| ?- constr(3,Y,Z).
clpz:(Z#=1#<==>_A),
clpz:(_B#=0#<==>_C),
clpz:(_D#=0#<==>_E),
clpz:(_F#=0#<==>_G),
clpz:(_H#=0#<==>_I),
clpz:(_C#//_E#<==>1),
clpz:(_G#//_I#<==>_A),
clpz:(Y mod 3#=_B),
clpz:(Y mod 3#=_F),
clpz:(Y mod 7#=_D),
clpz:(Y mod 7#=_H),
clpz:(Y in 3//5//7),
clpz:(Z in 1..2),
clpz:(_C in 0..1),
clpz:(_B in 0..2),
clpz:(_E in 0..1),
clpz:(_D in 0..6),
clpz:(_A in 0..1),
clpz:(_G in 0..1),
clpz:(_F in 0..2),
clpz:(_I in 0..1),
clpz:(_H in 0..6) ? ;
no

Y ahora agregando un solo objetivo:

| ?- constr(3,Y,Z), clpz:contracting([Z]).
Z = 1,
clpz:(_A#=0#<==>_B),
clpz:(_C#=0#<==>_D),
clpz:(_E#=0#<==>_F),
clpz:(_G#=0#<==>_H),
clpz:(_B#//_D#<==>1),
clpz:(_F#//_H#<==>1),
clpz:(Y mod 3#=_A),
clpz:(Y mod 3#=_E),
clpz:(Y mod 7#=_C),
clpz:(Y mod 7#=_G),
clpz:(Y in 3//5//7),
clpz:(_B in 0..1),
clpz:(_A in 0..2),
clpz:(_D in 0..1),
clpz:(_C in 0..6),
clpz:(_F in 0..1),
clpz:(_E in 0..2),
clpz:(_H in 0..1),
clpz:(_G in 0..6) ? ;
no

En otras palabras, una versión más consistente de su constr/3 predicado sería:

constr_better(X, Y, Z) :-
constr(X, Y, Z),
clpz:contracting([Z]).

Anteriormente, utilicé SICStus con la library(clpz) que es la sucesora de la library(clpfd) de SWI, que también tiene clpfd:contracting/1 .

Answer 3

Después de probar muchas cosas, terminé con estas conclusiones, dime si estoy equivocado (lo siento, soy un principiante).

Consideremos esta muestra:

:- use_module(library(clpfd)).
constr(X,Y,Z) :-
X in {1,2,3,4,5,6,7},
Y in {3,5,7,21,42},
Z in {1,2},
(X #= 3) #==> ((Y mod 3 #= 0) #// (Y mod 7 #= 0)),
(Z #= 1) #<==> ((Y mod 3 #= 0) #// (Y mod 7 #= 0)).
constr_better(X,Y,Z) :- constr(X,Y,Z), clpfd:contracting([X,Y,Z]).
res(X,L) :- setof(X, indomain(X), L).
constrChoice(X,Y,Z,XOut,YOut,ZOut) :-
constr(X,Y,Z),
res(X,XOut),res(Y,YOut),res(Z,ZOut).
constrChoiceBetter(X,Y,Z,XOut,YOut,ZOut) :-
constr_better(X,Y,Z),
res(X,XOut),res(Y,YOut),res(Z,ZOut).

1. constr(3,Y,Z) da Z in 1..2 pero constrChoice(3,Y,Z,Xout,Yout,Zout) da Zout=[1] , por lo que no es necesario utilizar contracting/1 porque el uso de setof/3 junto con indomain/1 hace el trabajo. No es necesario volver a escribir los predicados de prólogo tampoco.

2. Ahora si tengo AND #// lugar de OR #// , ninguna de las llamadas constr(3,Y,Z) , constrChoice(3,Y,Z,Xout,Yout,Zout) o constrChoiceBetter(3,Y,Z,Xout,Yout,Zout) da que Z debe ser 1. Efectivamente tengo que Y es 21 o 42, pero a Z se le dice que es 1 o 2. Lo que funciona: escriba que Y mod 21 #= 0 directamente, y luego no necesita usar contracting/1 tampoco.

Gracias por tus comentarios.