SWI-Prolog e vincoli, libreria CLP (FD)

Question

Sto giocando con i vincoli in (swi) prolog utilizzando la libreria clpfd.

Sto provando a identificare quando un insieme di vincoli incapsula o sussume l'altro, ad es. X < 4 incapsula X < 7 come ogni volta che il primo è vero, il secondo è vero. Questo può essere facilmente rappresentato usando implicazioni logiche. Tuttavia, non ho potuto ottenere l'operatore # == per darmi il risultato che volevo, quindi ho fatto ricorso a non usare (Co1 #/\ # \ Co2) dove Co1 e Co2 sono vincoli. Questo va bene per i vincoli individuali, ma poi ho voluto passare una congiunzione di vincoli in Co1 e Co2.

Ora ecco il problema. Quando provo

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

torno

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

(stranamente, a far questo in SICStus risultati in un errore di segmentazione)

Quando passo in

X#<7,X#<4 

I ottenere il desiderato

X in inf..3. 

Ovviamente, non posso passare quest'ultimo in (Co1 #/\ # \ Co2), ma il primo non mi dà il risultato che voglio. Qualcuno può spiegare perché i due approcci producono risultati diversi, e come posso convincere il primo ad agire come quest'ultimo?

Answer 1

Sembra che tu abbia a che fare con CLP (FD). Questi solutori distinguono la fase di impostazione e la fase di etichettatura per risolvere un problema di vincoli.

Un risolutore CLP (FD) non riduce completamente un problema durante la fase di configurazione. Dal momento che ha la possibilità di ridurre gli intervalli variabili durante la fase di etichettatura. Quindi potrebbe essere che durante l'installazione si pone un problema che potrebbe essere ridotto da altri solver a "No", ma non con un risolutore CLP (FD). Solo durante l'etichettatura verrà rilevato un "No".

Quanta riduzione viene eseguita durante la fase di configurazione dipende molto dal sistema CLP (FD) specificato. Alcuni sistemi CLP (FD) fanno più riduzione durante la fase di configurazione, mentre altri fanno meno. GNU Prolog ad esempio utilizza una propagazione indicizzata, mentre SWI Prolog no.Così troviamo, per esempio, non è il tuo esempio:

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 

Inoltre dal momento che si sta utilizzando vincoli reificati dipende anche un po 'come intelligente la reificazione è fatta. Ma immagino che nel caso presente sia solo una questione di propagazione. Troviamo ora il tuo esempio:

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) 

v'è un compromesso tra il fare di più la riduzione nella fase di messa a punto e lasciando più lavoro per il fase di etichettatura. E tutta la questione dipende anche dall'esempio dato. Ma quando si hanno anche l'etichettatura accanto l'installazione, non si vedrà alcuna differenza in termini di risultato:

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 

non ho la prova con SICStus Prolog o B-Prolog. Ma immagino che si comporteranno da qualche parte nelle vincite di SWI-Prolog e GNU Prolog.

CLP (Q) non è un'alternativa reale se il tuo dominio è in realtà FD, dal momento che mancherà alcune riduzioni "No", che CLP (FD) non mancherà. Per esempio il seguente è insoddisfacibile a CLP (FD), ma satisfiable in CLP (Q):

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

Bye

Answer 2

Il sottoinsieme dei vincoli aritmetici generali sugli interi è indecidibile in generale, quindi tutti i risolutori corretti hanno limiti intrinseci oltre i quali devono ritardare le loro risposte fino a quando non si conosce più. Se sai che i tuoi domini sono finiti, puoi pubblicare i domini e quindi provare a trovare dei controesempi che renderebbero l'implicazione non valida, usando il predicato di etichettatura/2 del risolutore di vincoli. Considera anche che le disuguaglianze lineari su Q sono decidibili e che la libreria SWI-Prolog (clpq) è completa per loro. Si può quindi provare i vostri vincoli nel CLP (Q) con:

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

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

e vedere che nessun controesempio esiste in Q (quindi anche non in Z), e, quindi, l'implicazione detiene.