制約プログラミングとSAT解決において、バックジャンプ(非時系列バックトラッキング[1]またはインテリジェントバックトラッキング[2]とも呼ばれる)は、検索空間を減らすバックトラッキング アルゴリズムの拡張機能です。変数のすべての値がテストされると、バックトラッキングは常に検索ツリーの1レベル上に進みますが、バックジャンプはより多くのレベルを上る場合があります。この記事では、変数の評価に固定順序が使用されていますが、動的な評価順序にも同じ考慮事項が適用されます。
-
通常のバックトラッキングで訪問される検索ツリー
-
バックジャンプ: 灰色のノードは訪問されない
意味
バックトラッキングで変数のすべての値を試しても解が見つからない場合、以前に割り当てられた最後の変数が再検討され、その値が変更されるか、他の値を試す必要がない場合はさらにバックトラッキングが行われます。 が現在の部分的な割り当てであり、 のすべての値を試しても解が見つからない場合、バックトラッキングでは、 を拡張する解は 存在しないと結論付けられます。次に、アルゴリズムは まで「進み」、可能であれば の値を変更し、そうでない場合は再度バックトラッキングを行います。
の部分的な割り当ては、 のどの値も解を導かないことを証明するために必ずしも完全に必要というわけではありません。特に、部分的な割り当てのプレフィックスが同じ特性を持つ場合があります。つまり、を拡張して のどのような値でも解を形成できないようなインデックスが存在します。アルゴリズムがこの事実を証明できる場合、通常のように を再検討するのではなく、の異なる値を直接検討できます。
-
への現在の割り当てが、 のあらゆる可能な値で試行されて失敗した例。 バックトラックは に戻り、新しい値を割り当てようとします。
-
アルゴリズムはバックトラックする代わりに、さらに詳細化を行い、評価 、 、 がどのソリューションの一部でもないことを証明します。
-
その結果、 の現在の評価はどの解の一部にもならず、アルゴリズムは に直接戻って、 の新しい値を試すことができます。
バックジャンプ アルゴリズムの効率は、バックジャンプできる高さに依存します。理想的には、アルゴリズムは からのどの変数にでもジャンプでき、 への現在の割り当てを拡張して の任意の値を持つソリューションを形成できないようにします。この場合、は安全なジャンプと呼ばれます。
ジャンプが安全かどうかの判定は、必ずしも実行可能ではありません。安全なジャンプは、アルゴリズムが見つけようとしているソリューションのセットに基づいて定義されるからです。実際には、バックジャンピング アルゴリズムは、安全なジャンプであると効率的に証明できる最も低いインデックスを使用します。アルゴリズムが異なれば、ジャンプが安全かどうかを判断する方法も異なります。これらの方法にはそれぞれ異なるコストがかかりますが、より安全なジャンプを見つけるためのコストが高くなると、検索ツリーの一部をスキップすることによる検索量の低下と引き換えに、コストが大きくなる場合があります。
葉ノードでのバックジャンプ
バックジャンプが可能な最も単純な条件は、変数のすべての値がそれ以上の分岐なしで矛盾していることが証明されている場合です。制約充足では、部分評価は、割り当てられた変数を含むすべての制約を満たす場合にのみ矛盾がなく、そうでない場合は矛盾します。割り当てられていない変数の一部は他の制約に違反することなく割り当てられない可能性があるため、矛盾のない部分的なソリューションを矛盾のない完全なソリューションに拡張できない場合があります。
特定の変数のすべての値が現在の部分解と一致しない状態は、リーフ デッド エンドと呼ばれます。これは、変数が検索ツリーのリーフ (この記事の図では、子としてリーフのみを持つノードに対応) である場合に発生します。
ジョン・ガシュニグによるバックジャンプアルゴリズムは、葉の行き止まりでのみバックジャンプを行います。[3]言い換えれば、すべての可能な値がテストされ、別の変数に分岐する必要なく矛盾した結果が出た場合にのみ、バックトラックとは異なる動作をします。
安全なジャンプは、あらゆる値 に対して、と矛盾するの最短の接頭辞を評価するだけで見つけることができます。言い換えると、 がの可能な値である場合、アルゴリズムは次の評価の一貫性をチェックします。
評価が矛盾する最小のインデックス(リストの一番下)は、 がの唯一の可能な値である場合に安全なジャンプになります。すべての変数は通常、複数の値をとることができるため、各値のチェックから得られる最大インデックスは安全なジャンプであり、John Gaschnig のアルゴリズムがジャンプするポイントです。
実際には、アルゴリズムは の一貫性をチェックすると同時に上記の評価をチェックすることができます。
内部ノードでのバックジャンプ
以前のアルゴリズムでは、変数の値が現在の部分的なソリューションと矛盾していることが判明した場合にのみ、それ以上の分岐を行わずにバックジャンプを行います。つまり、検索ツリーのリーフ ノードでのみバックジャンプが可能です。
検索ツリーの内部ノードは、前のノードと一致する変数の割り当てを表します。この割り当てを拡張するソリューションがない場合、前のアルゴリズムは常にバックトラックします。この場合、バックジャンプは実行されません。
内部ノードでのバックジャンプは、リーフノードの場合のようには実行できません。実際、分岐が必要な評価がいくつかある場合、それは現在の割り当てと一致しているためです。その結果、最後の変数のこれらの値と一致しないプレフィックスの検索は成功しません。
このような場合、現在の部分評価で評価がソリューションの一部ではないことを証明するのは、再帰検索です。特に、アルゴリズムは、ソリューションが見つかった後に停止するのではなく、このノードに戻るため、この時点からソリューションが存在しないことを「認識」します。
この戻りは、アルゴリズムが部分的なソリューションが矛盾していることが判明したポイントである、いくつかの行き止まりによるものです。さらにバックジャンプするために、アルゴリズムは、ソリューションを見つけることができないのはこれらの行き止まりによるものであることを考慮する必要があります。特に、安全なジャンプは、これらの行き止まりを依然として矛盾した部分的なソリューションにするプレフィックスのインデックスです。
-
この例では、矛盾が交差する 3 つのポイントがあるため、アルゴリズムは可能な値をすべて試した後、 に戻ります。
-
2番目の点は、変数の値とその部分評価から削除されたとしても矛盾したままです(変数の値は子変数にあることに注意してください)。
-
他の矛盾した評価は、、、およびがなくても変わらない。
-
これはすべての矛盾を維持する最も低い変数であるため、アルゴリズムは に戻ることができます。 の新しい値が試されます。
言い換えると、 のすべての値が試されたとき、の現在の真理値評価がノードの子孫であるリーフノード内のすべての の真理値評価と一致しない場合、アルゴリズムは前の変数に戻ることができます。
簡素化

のサブツリーには潜在的に多数のノードが存在するため、安全にバックジャンプするために必要な情報は、そのサブツリーの訪問中に収集されます。安全なジャンプの検索は、2 つの考慮事項によって簡素化できます。1 つ目は、アルゴリズムには安全なジャンプが必要ですが、可能な限り最高の安全なジャンプではないジャンプでも機能することです。
2 つ目の簡略化は、のバックジャンプを探す際に、バックジャンプによってスキップされた のサブツリー内のノードを無視できることです。より正確には、ノード からノード までのバックジャンプによってスキップされたすべてのノードは、をルートとするサブツリーとは無関係であり、それらの他のサブツリーも無関係です。
実際、アルゴリズムがパスを経由してノードからに下り、戻る途中でバックジャンプする場合、代わりに から に直接進むこともできたはずです。実際、バックジャンプは、との間のノードが をルートとするサブツリーとは無関係であることを示しています。言い換えると、バックジャンプは、検索ツリーの領域への訪問が間違いであったことを示しています。したがって、検索ツリーのこの部分は、 またはその祖先の 1 つからのバックジャンプの可能性を考慮するときに無視できます。

この事実は、各ノードで、そのノードをルートとするサブツリーにソリューションが存在しないことを証明するのに十分な評価を持つ、以前に割り当てられた変数のセットを収集することによって利用できます。このセットは、アルゴリズムの実行中に構築されます。ノードから取り消すと、このセットはノードの変数から削除され、バックトラックまたはバックジャンプの宛先のセットに収集されます。バックジャンプからスキップされたノードは決して取り消されないため、それらのセットは自動的に無視されます。
グラフベースのバックジャンプ
グラフベースのバックジャンプの原理は、どの変数がリーフ ノードでインスタンス化される変数との制約内にあるかをチェックすることで、安全なジャンプが見つかるというものです。すべてのリーフ ノードと、そこにインスタンス化されるインデックスのすべての変数について、その変数が との制約内にあるより小さいか等しいインデックスを使用して、安全なジャンプを見つけることができます。特に、 のすべての値が試された場合、このセットには、 をルートとするサブツリーにアクセスしても解決策が見つからないことが証明される評価が可能な変数のインデックスが含まれます。その結果、アルゴリズムはこのセットの最高のインデックスにバックジャンプできます。
バックジャンプによってスキップされたノードは、さらなるバックジャンプを考慮するときに無視できるという事実は、次のアルゴリズムによって利用できます。リーフ ノードから後退する場合、そのノードに制約されている変数のセットが作成され、その親、またはバックジャンプの場合は祖先に「送り返されます」。すべての内部ノードで、変数のセットが維持されます。子または子孫のいずれかから変数のセットが受信されるたびに、それらの変数は維持されているセットに追加されます。ノードからさらにバックトラックまたはバックジャンプする場合、ノードの変数はこのセットから削除され、セットはバックトラックまたはバックジャンプの宛先であるノードに送信されます。このアルゴリズムが機能するのは、ノードで維持されているセットが、このノードの子孫であるリーフで不満足性を証明するために関連するすべての変数を収集するためです。変数のセットはノードから戻るときにのみ送信されるため、バックジャンプによってスキップされたノードで収集されたセットは自動的に無視されます。
対立に基づくバックジャンプ
競合ベースのバックジャンプ (別名、競合指向バックジャンプ) は、より洗練されたアルゴリズムであり、より大きなバックジャンプを実現できる場合があります。これは、同じ制約に 2 つの変数が共通に存在するかどうかだけでなく、制約が実際に矛盾を引き起こしたかどうかもチェックすることに基づいています。特に、このアルゴリズムは、すべてのリーフで違反した制約の 1 つを収集します。すべてのノードで、リーフで収集された制約の 1 つにある変数の最高インデックスが安全なジャンプです。
各リーフで選択された違反制約は、結果として生じるジャンプの安全性には影響しませんが、可能な限り最高のインデックスの制約を選択すると、ジャンプの高さが増します。このため、競合ベースのバックジャンプでは、より低いインデックスの変数に対する制約がより高いインデックスの変数に対する制約よりも優先されるように制約が順序付けられます。
正式には、 にあるが にはない変数の最高インデックスが、にあるが にはない変数の最高インデックスよりも低い場合、ある制約は別の制約よりも優先されます。つまり、共通変数を除いて、すべてのインデックスが低い制約が優先されます。
リーフ ノードでは、アルゴリズムは、リーフで最後に評価された変数と矛盾しない、最も低いインデックスを選択します。この評価で違反された制約の中で、最も好ましいものを選択し、 未満のすべてのインデックスを収集します。このようにして、アルゴリズムが変数 に戻ったときに、収集された最も低いインデックスによって安全なジャンプが識別されます。
実際には、このアルゴリズムは、 のすべての値に対してセットを作成する代わりに、すべてのインデックスを単一のセットに収集することによって簡略化されます。特に、アルゴリズムは、各ノードで、バックジャンプによってスキップされていない子孫からのすべてのセットを収集します。このノードから撤回すると、このセットはノードの変数から削除され、バックトラックまたはバックジャンプの宛先に収集されます。
制約充足問題に対するコンフリクト指向バックジャンピングは、パトリック・プロッサーが1993年に発表した論文[4]で提案された。
参照
参考文献
- ^ Möhle, S., & Biere, A. (2019). バックトラッキングのバックアップ。Theory and Applications of Satisfiability Testing–SAT 2019: 22nd International Conference、SAT 2019、ポルトガル、リスボン、2019年7月9日~12日、Proceedings 22 (pp. 250-266)。Springer International Publishing。
- ^ Dechter, Rina (2003). 制約処理. Morgan Kaufmann.
- ^ Gaschnig, J. 1977. ほとんどの冗長なテストを排除する一般的なバックトラックアルゴリズム。IJCAI-77、vol. 1、457
- ^ Prosser, Patrick (1993). 「制約充足問題のためのハイブリッドアルゴリズム」(PDF). 計算知能 9(3).
文献
- デヒター、リナ (2003)。制約処理。モーガン・カウフマン。ISBN 1-55860-890-7。
- プロッサー、パトリック(1993)。「制約充足問題のためのハイブリッドアルゴリズム」(PDF)。計算知能9(3)。
