理論的/実際的な問題があり、管理方法については今のところ手がかりがありません。
私は、遺伝学アルゴリズムを使用して、CのCNF問題に当てはまらないモデルが存在する場合はそのモデルを見つけ、矛盾を証明できるSAT ソルバーを作成します。
SAT-problem は、基本的にこの種の問題のように見えます:
私の目標は、このソルバーを使用して、さまざまな NP-completes問題の解決策を見つけることです。基本的に、さまざまな問題を SAT に変換し、ソルバーで SAT を解き、その解を元の問題に受け入れられる解に変換します。
私はすでに N*N Sudoku と N-queens 問題に成功していますが、ここに私の新しい目標があります: クラススケジューリング問題を SAT に減らすことですが、簡単に変換するためにクラススケジューリング問題を形式化する方法がわかりません後にSATでそれ。
目標は明らかに、数か月で次のようなスケジュールの図を生成することです。
残念ながら、クラススケジューリングを解決できるこのソースコードを見つけましたが、残念ながらSATへの削減はありません:/
計画全般に関する記事もいくつか見つけました (たとえば、 http: //www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf)。
しかし、この記事で使用されている計画ドメイン定義言語は、クラス スケジューリングの問題を表すにはあまりにも一般的すぎるように思えます。:/
Class-scheduling を SAT に減らした後、SAT ソリューション (存在する場合は ^^) を Class-schedule に変換するために効率的に形式化する方法について、誰かがアイデアを持っていますか?
私は基本的にどんな提案にもオープンです。今のところ、どのように表現するか、問題を減らす方法、SATソリューションをスケジュールに変換する方法についてはわかりません...
フォローアップの質問:ブール充足可能性へのクラス スケジューリング [多項式時間削減] パート 2