SWI-Prolog和約束，庫CLP（FD）

Question

我在（swi）prolog中使用clpfd庫約束玩弄。

我試圖確定何時一組約束封裝或包含另一組約束如果前者爲真，則後者爲真。這可以用邏輯蘊涵來表示。然而，我不能讓＃==>操作符給我我想要的結果，所以我使用了不是（Co1＃/ \＃\ Co2），其中Co1和Co2是約束條件。這對個人的約束條件很好，但我希望將約束連接傳遞給Co1和Co2。

現在，這是蹭。當我嘗試

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

我回來

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

（奇怪的是，在Sicstus導致分段錯誤這樣做）

當我通過在

X#<7,X#<4 

我得到想要的

X in inf..3. 

顯然，我不能把後者變成不是（Co1＃/ \＃\ Co2），但前者並沒有給我想要的結果。任何人都可以解釋爲什麼這兩種方法會產生不同的結果，以及我如何讓前者像後者一樣行事？

Answer 1

看來你正在與CLP（FD）打交道。這些求解器區分設置階段和解決約束問題的標註階段。

CLP（FD）求解器在設置階段並未完全減少問題。因爲它有機會在貼標籤階段減少可變範圍。因此，在安裝過程中可能會出現一個問題，可能會被其他求解器降低爲「否」，但不會使用CLP（FD）解算器。只有在標籤過程中才會檢測到「否」。

在設置階段完成多少減少很大程度上取決於給定的CLP（FD）系統。一些CLP（FD）系統在設置階段進行更多的減少，而其他的則更少。例如，GNU Prolog使用一些索引傳播，而SWI Prolog則不使用。因此我們發現，例如，沒有你的例子：

SWI-Prolog的：

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

GNU序言：

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

另外，由於使用的是物化的限制也要看一點點有多聰明物化完成。但我猜在目前的情況下，它只是一個傳播問題。我們現在找到你的例子：

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序言：

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

有這樣的設置階段更加減少，留下更多的工作之間的權衡標籤階段。整個事情也取決於給定的例子。但是，當你還設置旁邊標註，你不會看到在結果方面的任何差異：

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序言：

?- 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 

我沒有測試使用SICStus Prolog或B-Prolog。但我想他們會在SWI-Prolog和GNU Prolog的合適位置上表現出色。

如果你的域是真正的FD，CLP（Q）是沒有真正的選擇，因爲它會錯過一些「否」減少，CLP（FD）不會錯過。例如，下面是CLP（FD），不可滿足的，但CLP（Q）可滿足：

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

再見

Answer 2

對整數的一般算術約束的包含通常是不可判定的，因此所有正確的求解器都有內在的限制，超過這些限制，他們必須延遲其答案，直到更多人知道。如果你知道你的域名是有限的，你可以發佈域名，然後嘗試使用約束求解器的標籤/ 2謂詞找到會導致蘊含無效的反例。考慮到Q上的線性不等式是可確定的，並且SWI-Prolog的庫（clpq）對它們來說是完整的。因此，你可以嘗試在CLP（Q）與約束：

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

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

，看到沒有這樣的反Q中存在的（因此也沒有Z），因而蘊涵成立。