5

clpfd ライブラリを使用して (swi) プロローグで制約をいじっています。

ある制約セットが他の制約セットをカプセル化または包含している場合を特定しようとしています。たとえば、前者が true の場合は常に後者が true であるため、X<4 は X<7 をカプセル化します。これは、論理的含意を使用して簡単に表すことができます。ただし、 #==> 演算子を使用しても希望どおりの結果が得られなかったため、not(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.

明らかに、後者を not(Co1 #/\ #\Co2) に渡すことはできませんが、前者では必要な結果が得られません。2 つのアプローチが異なる結果をもたらす理由と、前者を後者のように動作させる方法を説明できる人はいますか?

4

2 に答える 2

3

整数に対する一般的な算術制約の総和は一般に決定不可能であるため、すべての正しいソルバーには固有の制限があり、それを超えると、より多くのことがわかるまで答えを遅らせる必要があります。ドメインが有限であることがわかっている場合は、ドメインを投稿してから、制約ソルバーの labeling/2 述語を使用して、含意を無効にする反例を見つけようとすることができます。Q 上の線形不等式は決定可能であり、SWI-Prolog のライブラリ (clpq) はそれらに対して完全であることも考慮してください。したがって、次のように CLP(Q) で制約を試すことができます。

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

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

そして、そのような反例は Q には存在しない (したがって Z にも存在しない) ことを確認してください。したがって、含意が成り立ちます。

于 2010-11-04T20:24:31.960 に答える
2

あなたはCLP（FD）を扱っているようです。これらのソルバーは、制約問題を解決するセットアップ フェーズとラベル付けフェーズを区別します。

CLP(FD) ソルバーは、セットアップ段階で問題を完全に軽減するわけではありません。ラベル付け段階で変数範囲を減らす可能性があるためです。したがって、セットアップ中に問題が発生し、他のソルバーによって「いいえ」に削減される可能性がありますが、CLP(FD) ソルバーではそうではありません。ラベル付け中のみ「いいえ」が検出されます。

セットアップ段階でどの程度の削減が行われるかは、特定の CLP(FD) システムに大きく依存します。一部の CLP(FD) システムは、セットアップ段階でより多くの削減を行いますが、他のシステムはより少ない削減を行います。たとえば、GNU Prolog はいくつかのインデックス伝播を使用しますが、SWI Prolog は使用しません。したがって、たとえば、あなたの例ではありません。

SWI-プロローグ:

?- 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-プロローグ:

?- 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-プロローグ:

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

さよなら

于 2012-06-22T10:25:49.973 に答える