一系列約束是另一系列的一個子集嗎？

Question

我有兩個系列的約束S和S'，他們描述可能無限大的集合。說例如S：x <= 10 and y <= x和S'：x <= 20 and y <= 20。 現在我想知道如果S是S'的子集？

我以爲我可以嘗試解決類似於：S' and not (S and S')，如果它找不到解決方案S是S'的子集。

我怎麼會把這個在序言中，這是一個可靠的解決方案？ 我正在使用gprolog，但我可以切換到另一個實現。

Answer 1

通過@false的評論是正確的，據我可以看到：給予二套小號和小號「：如果小號是小號一個子集」，那麼補的交集的小號「和小號應該是空集（也有小號外沒有任何元素」即是S-的元件）。

看來，constraint programming over finite domains應該做的伎倆，如果你正在處理整數。使用SWI-Prolog的7.3，並手動做你的榜樣，我得到：

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

?- \+ (X #=< 10, Y #=< X, #\ X #=< 20 #\/ #\ Y #=< 20). 
true. 

第二個查詢應爲：

\+ (% succeed if no solutions 
    X #=< 10, Y #=< X, % set S and... 
    #\ X #=< 20 #\/ #\ Y #=< 20 % complement of set S' (De Morgan's Law) 
). 

我認爲，小號補「可能也被寫入如：

\# (X #=< 20 #/\ Y #=< 20) 

如果你想有一個更通用的解決方案，你就必須想出一個辦法找到約束的任意一組的補秒。請注意，可以使用Prolog連詞（逗號）作爲邏輯AND，但不能將該分隔用作OR。