Minisat は制約プログラミング/満足度ツールです。ブラウザで動作するバージョンの Minisat があります http://www.msoos.org/2013/09/minisat-in-your-browser/
Minisat でスケジューリングの問題を表現するにはどうすればよいですか? Minisat にコンパイルして表現できる高水準言語はありますか?
試験の時間割などの問題を解決することを意味します。http://docs.jboss.org/drools/release/6.1.0.Final/optaplanner-docs/html_single/#examination
もう 1 つの高レベル モデリング言語は Picat ( http://picat-lang.org/ ) です。これには、sat モジュールを使用するときに、solve/2 を CNF に変換するオプションがあります (例: "solve([dump], Vars)")。sat モジュールを使用する場合の構文は、cp および mip モジュールと同様に、標準の CLP 構文に似ています。
Picat の例については、私の Picat ページ ( http://hakank.org/picat/ ) を参照してください。
MinisatやCryptominisatなどのSAT ソルバーORは通常、論理式の節セットを結合正規形 (CNF)で読み取ります。問題をこの CNF 形式に変換するには、エンコード手順が必要です。
Circuit SAT ソルバーは、 ではなく、ネストされたブール式を処理しCNFます。しかし、最近では、このタイプのソルバーよりもソルバーの方が優れているようCNF SATです。
Minizincのような制約プログラミング ソルバーは、書きやすく、理解しやすい高水準言語を使用します。使用されている機能に応じて、Minizincは入力言語をCNF/DIMACSSAT ソルバーに適した形式に変換できます。
Peter Stuckey の論文「There are no CNF Problems」では、この考えが説明されています。彼のスライドには、スケジューリングに関するいくつかの洞察も含まれています。
Hakan Kjellerstrandによって書かれたスケジューリングのためのMinizinc の例を見てください。
Emmanuel Hebrard のScheduling and SATは、このトピックを広範囲に扱っています。
私は数ヶ月前にこのプロジェクトに取り組みました。
するのは本当に面白かったです。
miniSAT (またはその他の SAT ソルバー) を使用するには、スケジューリング問題を SAT 問題に変換する必要があります。
私が 3 つのパートで行ったこの質問をお勧めします。
ブール充足可能性へのクラス スケジューリング [多項式時間削減]
ブール充足可能性へのクラス スケジューリング [多項式時間削減] パート 2
ブール充足可能性へのクラススケジューリング [多項式時間削減] 最終パート
そして、基本的に、スケジューリング問題を MiniSAT が読み取って解決できる SAT 問題に変換する方法を段階的に説明します :)。
このプロジェクトで非常に大きな助けとなった @ amitに改めて感謝します。
この答えがあれば、S の科目を G の異なるグループの生徒に教えている T の教師がいる N の部屋を解決することができます :) これで、スケジューリングの問題の 99% を解決できます。