0

私は現在、試験のために2SATの問題を研究していますが、力ずくで解決策が存在するかどうかを確認する方法がよくわかりません。これは少し奇妙に思えますが、含意グラフをもう少しうまく実装する方法は理解していますが、ブルートフォース戦略を実装する方法がよくわかりません。

誰かがいくつかの洞察を共有できますか？たぶん擬似コードかJavaで。

ありがとう

4

2 に答える 2

2

数式の変数は、整数値のビットとしてエンコードできます。次に、力ずくの方法は、積分「コンテナ」が取る可能性のあるすべての可能な値の範囲に要約されます。

つまり、数式のすべての変数を表す整数の配列があり、キャリーを使用して整数をインクリメントし、各ステップで、数式に対してそれが表す解を確認します。解決策が一致したら停止します。

このような変数コンテナの非常に単純な実装は次のとおりです。

class OverflowException extends RuntimeException {}

public class Variables {
    int[] data;
    int size;

    public Variables(int size_){
        size = size_;
        data = new int[1 + size/32];
    }
    public boolean get(int i){
         return (data[i/32] & (1 << i%32)) != 0;
    }
    public void set(int i, boolean v){
        if (v)
            data[i/32] |= (1 << i%32);
        else
            data[i/32] &= ~(1 << i%32);
    }
    public void increment(){
         int i;
         for (i=0; i < size/32; i++){
             data[i]++;
             if (data[i] != 0) return;
         }
         if (size%32 != 0){
             data[i]++;
             if ((data[i] & ~((1 << (size%32)) - 1)) != 0)
                 throw new OverflowException();
        }
    }
}

（警告エンプター：コードはテストされていません）。

変数配列は、より単純にコンテナーとして表すこともできますが、増分ステップのためにパフォーマンスが少し低下する可能性があります（ただし、増分操作にプレーンバイナリエンコーディングの代わりにグレイコードbooleanを使用することで軽減できる可能性がありますが、この実装の複雑さは逆のことを示しているようです。複雑なソリューションを選択する場合は、代わりに優れたsat2ソルバーになる可能性があります）。

于 2013-02-08T20:15:18.703 に答える
0

これが、ブルートフォースソリューションを使用しない理由です:)、多くのリソースを消費します。私のアルゴリズムは、すべての可能性を備えたマトリックスを作成することではありません。ただし、1つの割り当てを作成し、すぐにテストします。次に、次のものを作成します。最初の解決策が見つかったら停止できます。

于 2013-02-08T19:16:40.087 に答える