Loading article…
制約プログラミングやSATソルビングにおいて、バックジャンピング（非時系列バックトラッキング[ 1 ]またはインテリジェントバックトラッキング[ 2 ]とも呼ばれる）は、探索空間を縮小するバックトラッキングアルゴリズムの改良版である。バックトラッキングは、変数のすべての値がテストされると常に探索ツリーを1レベル上回るが、バックジャンピングはそれ以上のレベル上回る可能性がある。本稿では、変数の評価順序を固定する。が使用されるが、動的な評価順序にも同様の考慮事項が適用される。
バックトラッキングが変数に対してすべての値を試しても解が見つからない場合、以前に割り当てられた最後の変数を再検討し、その値を変更するか、他に試すべき値がない場合はさらにバックトラッキングを行います。現在の部分割り当てとすべての値は解決策が見つからずに試された結果、バックトラッキングでは拡張する解決策はないと結論付けられました 存在する。アルゴリズムは次に「上昇」する。変化可能であればその値を取得し、そうでなければ再び後戻りする。
部分割り当ては、値が存在しないことを証明するために必ずしも完全に必要ではありません。解決策につながる。特に、部分代入の接頭辞は同じ性質を持つ可能性がある。つまり、インデックスが存在する。そのためどのような値であっても、解を形成するように拡張することはできませんアルゴリズムがこの事実を証明できれば、別の値を直接考慮することができます。再考する代わりに通常通りの行動をとるだろう。
バックジャンピングアルゴリズムの効率は、どれだけ高くバックジャンピングできるかに依存します。理想的には、アルゴリズムはどの変数に対しても現在の割り当てはいかなる値でも解を形成するように拡張することはできませんもしそうであれば、これは安全なジャンプと呼ばれます。
ジャンプが安全かどうかを判断することは必ずしも容易ではありません。なぜなら、安全なジャンプはアルゴリズムが探そうとしている解の集合に基づいて定義されるからです。実際には、バックジャンピングアルゴリズムは、安全にジャンプできると効率的に証明できる最小のインデックスを使用します。アルゴリズムによって、ジャンプが安全かどうかを判断する方法は異なります。これらの方法にはそれぞれ異なるコストがかかりますが、より高い安全なジャンプを見つけるためのコストが高くても、探索ツリーの一部をスキップすることで探索量を減らすことができる場合があります。
バックジャンピングが可能な最も単純な条件は、変数のすべての値がそれ以上の分岐なしに矛盾していることが証明された場合です。制約充足においては、部分評価は、割り当てられた変数に関するすべての制約を満たす場合に限り整合して おり、そうでない場合は矛盾しています。割り当てられていない変数の一部は、他の制約に違反することなく割り当てることができない可能性があるため、整合的な部分解を整合的な完全解に拡張できない場合があります。
特定の変数のすべての値が現在の部分解とは矛盾しているこれはリーフ行き止まりと呼ばれます。これは変数がは探索木の葉ノードです（この記事の図では、子ノードとして葉ノードのみを持つノードに対応します）。
ジョン・ガシュニグによるバックジャンピングアルゴリズムは、葉の行き止まりでのみバックジャンピングを実行します。[ 3 ]言い換えれば、すべての可能な値がテストを行った結果、別の変数で分岐する必要なく一貫性のない結果となった。
安全なジャンプは、各値に対して単純に評価することで見つけることができます。の最短の接頭辞矛盾するつまり、は、このアルゴリズムは、以下の評価の一貫性をチェックします。
評価が一貫していない最小のインデックス（リストの最低値）は、安全なジャンプとなるでしょう。は、唯一の可能な値でした。。通常、すべての変数は複数の値を取ることができるため、各値のチェックから得られる最大インデックスは安全なジャンプ先であり、ジョン・ガシュニグのアルゴリズムがジャンプするポイントとなります。
実際には、アルゴリズムは、一貫性をチェックしながら、上記の評価を同時にチェックすることができます。。
従来のアルゴリズムでは、変数の値が現在の部分解と矛盾することが、それ以上の分岐なしに示された場合にのみ、バックジャンプが行われます。つまり、探索木の葉ノードでのみバックジャンプが可能です。
探索木の内部ノードは、前の変数と整合性のある変数の割り当てを表します。この割り当てを拡張する解が存在しない場合、前のアルゴリズムは常にバックトラックします。この場合、バックジャンプは行われません。
内部ノードでのバックジャンプは、リーフノードの場合のように行うことはできません。実際、必要な分岐が行われないのは、それらが現在の割り当てと整合しているためです。その結果、最後の変数のこれらの値と整合しない接頭辞を検索しても成功しません。
このような場合、評価が証明されたのは現在の部分的な評価では解決策の一部にはならないこれは再帰探索です。特に、このアルゴリズムは、解が見つかった後に停止するのではなく、このノードに戻ってくるため、この時点から先は解が存在しないことを「認識」しています。
この戻りは、アルゴリズムが部分解が矛盾していると証明した行き止まり、つまり多数の行き止まりが原因です。さらにバックジャンプを行うには、アルゴリズムは解が見つからない原因がこれらの行き止まりにあることを考慮に入れる必要があります。特に、安全なジャンプ先は、これらの行き止まりを依然として矛盾した部分解にする接頭辞のインデックスです。
言い換えれば、すべての値が試行済み、アルゴリズムは前の変数にバックジャンプできるただし、現在の真実評価はは、すべての真理評価と矛盾するノードの子孫であるリーフノード。
サブツリー内のノード数が潜在的に多いため安全にバックジャンプするために必要な情報は、その部分木を訪問中に収集されます。安全なジャンプを見つけることは、2 つの考慮事項によって簡略化できます。1 つ目は、アルゴリズムは安全なジャンプを必要としますが、可能な限り高い安全なジャンプではないジャンプでも機能するということです。
2 つ目の簡略化は、サブツリー内のノードがバックジャンプによってスキップされたものは、バックジャンプを探す際に無視することができます。より正確には、ノードからのバックジャンプによってスキップされたすべてのノードノードまで根元がまた、それらの他のサブツリーも無関係である。
実際、アルゴリズムがノードからダウンした場合に経路を経由するが、戻る途中でバックジャンプする、その後直接に代わりに。実際、バックジャンプは、ノード間のそして根元が言い換えれば、バックジャンプは、探索ツリーの領域への訪問が間違いであったことを示しています。したがって、バックジャンプの可能性を考慮する際には、探索ツリーのこの部分は無視できます。あるいは、その祖先のいずれかから。
この事実を利用するには、各ノードに、そのノードを根とする部分木に解が存在しないことを証明するのに十分な、事前に割り当てられた変数のセットを収集します。このセットはアルゴリズムの実行中に構築されます。ノードから引き戻す際には、このセットからノードの変数が削除され、バックトラッキングまたはバックジャンプの宛先のセットに収集されます。バックジャンプからスキップされたノードは引き戻されることがないため、そのノードのセットは自動的に無視されます。
グラフベースのバックジャンピングの根拠は、どの変数が安全かをチェックすることで安全なジャンプを見つけることができるという点にある。変数との制約関係にあるリーフノードでインスタンス化されるもの。すべてのリーフノードとすべての変数についてインデックスのそこでインスタンス化されるインデックスは以下です。その変数は制約条件に含まれている安全なジャンプを見つけるために使用できます。特に、すべての値がが試されました。このセットには、評価によって、根が のサブツリーを訪ねても解が見つからないことを証明できる変数のインデックスが含まれています。その結果、アルゴリズムはこのセットの中で最も高いインデックスまで戻ることができる。
バックジャンプによってスキップされたノードは、さらにバックジャンプを行う際に無視できるという事実は、次のアルゴリズムで利用できます。リーフノードから引き返す際、そのノードと制約関係にある変数のセットが作成され、その親ノード（バックジャンプの場合は祖先ノード）に「送り返されます」。各内部ノードには、変数のセットが保持されています。子ノードまたは子孫ノードのいずれかから変数のセットが受信されるたびに、それらの変数が保持されているセットに追加されます。ノードからさらにバックトラックまたはバックジャンプを行う場合、ノードの変数はこのセットから削除され、セットはバックトラックまたはバックジャンプの宛先ノードに送信されます。このアルゴリズムが機能するのは、ノードで保持されているセットが、そのノードの子孫であるリーフノードの充足不可能性を証明するために必要なすべての変数を収集しているためです。変数のセットはノードから引き返すときにのみ送信されるため、バックジャンプによってスキップされたノードで収集されたセットは自動的に無視されます。
競合ベースのバックジャンピング（競合指向バックジャンピングとも呼ばれる）は、より洗練されたアルゴリズムであり、より大きなバックジャンピングを実現できる場合がある。このアルゴリズムは、2つの変数が同じ制約に共通して存在するかどうかだけでなく、その制約が実際に矛盾を引き起こしたかどうかもチェックする。具体的には、このアルゴリズムは、違反した制約のうちの1つを各リーフノードに収集する。各ノードにおいて、リーフノードに収集された制約のいずれかに含まれる変数のインデックスが最も高いものが、安全なジャンプ先となる。
各リーフで選択された違反制約は、結果として生じるジャンプの安全性には影響しませんが、可能な限り高いインデックスの制約を選択すると、ジャンプの高さが高くなります。このため、競合ベースのバックジャンピングでは、インデックスの低い変数に対する制約が、インデックスの高い変数に対する制約よりも優先されるように制約の順序が決定されます。
形式的には、制約他のものよりも好ましい変数の最高インデックスがしかし、変数の最高インデックスよりも低いしかし、つまり、共通変数を除けば、すべてのインデックスが小さい制約が好ましい。
葉ノードでは、アルゴリズムは最小のインデックスを選択します。そのためは、リーフで最後に評価された変数と矛盾しています。この評価で違反している制約の中から、最も好ましいものを選択し、以下のすべてのインデックスを収集します。こうすることで、アルゴリズムが変数に戻るときに収集されたインデックスの中で最も低い値が、安全なジャンプを示します。
実際には、このアルゴリズムは、すべてのインデックスを単一のセットに収集することで簡略化され、各値に対してセットを作成する代わりに、特に、このアルゴリズムは各ノードにおいて、バックジャンプによってスキップされなかった子孫ノードからのすべてのセットを収集します。このノードから戻る際、このセットはノードの変数から削除され、バックトラッキングまたはバックジャンプの宛先に収集されます。
制約充足問題に対するコンフリクト指向バックジャンピングは、パトリック・プロッサーが1993年の画期的な論文で提案した。[ 4 ]
