問題タブ [sat]

これが私の最初の質問の続きです（フローショップからブール充足可能性へ[多項式時間削減]）。

何かが間違っていて、正確な場所を知ることができなかったからです。もう一度、StackOverFlow の達人の助けを求めます :)

私が今持っているものの要約のために：

• 次のような入力ファイルがあります。

代表者 : 3 つのジョブ、2 つのショップ (機械)、および各ショップ (機械) での各ジョブの期間。そして、これらの問題について、最適な C_max 値を見つけたいと思っています。

したがって、たとえば、次の結果が出力されます (paint.exe xD で申し訳ありません)。

したがって、これらのファイルを読み取るために、次のようなリソースと問題の2つの構造を作成します。

読み取りは問題なく、構造内の入力ファイルにすべての情報があります。

この最適な問題 (最善の解決策を見つける) を決定問題 (これは可能な解決策ですか?) に変換したいと考えています。このための私の目標は、JobShop/FlowShop の問題を SAT 問題に変換することです。

• 私の目標は次のとおりです。C_max の値を固定し、SAT 問題を作成し、SAT ソルバーが問題に解決策がないことを示すまで C_max を減らします。解のある最後の値が最適値になります。

@Jens Schauder のおかげで、解決策が始まりました。私のブール変数は次のようなものです: s_1_2_3 with the meaning resource one gets used at machine 2 starting from time 3.

したがって、J 件の仕事、M 件のショップがあり、C_max の値を C にすると、次のJ * M * Cブール値変数が確実に得られます。

問題: 今のところ、私の SAT 問題は間違っています。与えられた解決策は大丈夫ではありません。

ここに私が今持っている制約があります：（Vは「OR」を意味し、他の：「そして」を意味します）

これは、私が一度に 1 つのショップでしか働けないことを意味します k

つまり、ショップ j は、時間 k に 1 つのジョブしか処理できません。

つまり、ジョブの期間が 1 を超える場合は、継続的でなければなりません。したがって、1 つの変数が true の場合、タスクの期間が終了するまで他の変数も true である必要があります。

問題の定式化について私が正しいかどうか、または/および制約を忘れたかどうかはよくわかりません。

今のところ、Job Shop も気にします (Flow Shop は基本的に同じで、ジョブはすべてのショップで同じ順序でなければなりません)。

非常に大きな質問で申し訳ありませんが、この種の問題については、それが何であるかを知るためにすべての詳細を用意することをお勧めします.

編集

上記の 3 つの制約のソース コードを追加します。内部で何かが間違っている可能性があり、何がわかりません...

制約 n°1 :

制約 n°2 :

制約 n°3 :

今、私はSAT解法について書いていますが、ある時点で立ち往生しています。あなたが私を助けてくれることを願っています。

SAT-Problems を解決するいくつかの方法について説明したいと思います。現在、次の 3 つの方法があります。

1. 強引な
2. ランダム (ナイーブ)
3. DPLL (ヒューリスティックが異なる)
4. ? ない ？
5. ...

私の問題は、唯一の効果的なアルゴリズムが DPLL (および DPLL とはわずかに異なる他のアルゴリズム) であることです。したがって、DPLL と比較するものは何もありません。

私の質問: 比較できる DPLL (DP) に基づいていないアルゴリズムをいくつか教えていただければ幸いです。

以下は私が見つけたもののいくつかです。

• モニエン・スペッケンマイヤー
• ダンツィン、ゲルト、ヒルシュ、シェーニング
• Paturi-Pudlák-Zane-アルゴリズム
• ホフマイスター、シェーニング、シューラー、渡辺

ご協力いただきありがとうございます。

特定のスイッチング ファブリックの同時ルートと必要な接続のリストを決定するためのプログラム/ライブラリ/アイデアを探しています。

ルートは交差せず、同時である必要があります。これは、実際の電気信号がリレーを介して送信される回線交換システムです。

この図では、1-4、5-2、および 4-5 がルーティングされていますが、マルチ終端接続 (1-1、2、3 など) も可能です。

ファブリックのトポロジーは約 200 ノードですが、単純なクロスバー構成ではありません。

また、一部のスイッチは一緒にしかオンまたはオフにできないため、追加の制約があります。

最後に、ソフトな制約として、最小量のスイッチを通るルートを優先するというものがありますが、複数の入力が 1 つの出力に接続されている場合、ラインはできるだけ出力の近くで合流する必要があります。(クロスバーの図では機能しませんが、入力 4 (緑) と 5 (緑) の両方が出力 3 (青) に接続されていると想像してください。4 と 5 は入力の近くでマージして、一緒にルーティングすることができます)。出力 3 に接続しますが、それらを個別にルーティングして、できるだけ 3 の近くでマージすることをお勧めします。

よりも良い

これは制約ソルバーにとって非常に単純な問題だと思いますが、開始方法がわかりません (どのソルバーですか? / 問題の説明をモデルに変換する方法は?)。

ここの表に従って値の置換を実行する関数を定義するにはどうすればよいですか?

私は一日中それについて考えていましたが、役に立つために、私はまだこの問題に固執しています. 提案/回答は大歓迎です。ありがとう！

k 個の単項節と 2 つの節しかない SAT インスタンスの複雑さは?

この結果の論文を見つけたいと思います.. 問題が少し異なる論文を 1 つ見つけました。すべての変数は最大で 2 回表示されます ...