問題タブ [sat]

このサイトの範囲から少し外れているかもしれませんが、ここにいる十分な数の人がこれを知っているので、試してみることにしました.

3-CNF 句のセットがあるとします

各変数範囲オーバー{0,1}

S にとって満足のいく割り当てはいくつありますか? 一般に、S のサイズが k の場合、S に対して満足のいく割り当てはいくつありますか?

これは、数を数えるということと同じくらい、3 選言節に対する満足のいく代入とは何かについての質問です。たとえば、 があるだけの場合、2 ³ = 8 通りの代入が可能です。

しかし、これらのうちどれが満足のいく割り当てですか?

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

一般的な問題

push-popすでにポップされcheck-satたスコープが、後続のスコープで必要な時間に影響を与えているように見えることに何度か気付きました。

つまり、それぞれが check-sat コマンドを含む複数の (場合によっては任意にネストされた) push-pop スコープを持つプログラムを想定します。さらに、2 番目のチェック サットには 10 秒かかり、最初のチェック サットには 0.1 秒しかかからないと仮定します。

最初の push-pop スコープにコメントした後、2 番目の check-sat は 1 しかかかりません。何故ですか？

• 私の知る限り、プッシュポップスコープが使用されている場合、Z3はインクリメンタルソルバーに切り替わります。なぜ彼らがこのように振る舞うのか（概念的な）理由はありますか？

• Z3 は重要度によってシンボルを属性付けすると聞いたことがあるが、これはプルーフ サーチに影響を与える (シンボルの重要度はプルーフ サーチ中にも変化する可能性がある)。それが理由でしょうか？(スコープ間で) 重要度をリセットすることは可能ですか?

• バグでしょうか？Leonardo が関連していると思われるバグについて言及しているこの投稿を見つけました (ただし、彼の回答は 2012 年のものです)。

特定のインスタンス

残念ながら、動作を説明するかなり長い (自動生成された) SMTLibファイルしかありません。量指定子と解釈されない関数を使用しますが、mbqi配列やビット ベクトルも使用しません。この例は、148 個のネストされたプッシュ/ポップ スコープと 89 個のチェック サットで構成されており、Z3 4.3.2 では処理に約 8 秒かかります。最後のチェックサット (接頭辞echo) は、はるかに長くかかります。

ランダムにいくつかのプッシュ/ポップ スコープにコメントを付けました (一度に 1 つずつ、最後のものではなく、シンボル宣言にコメントしないように注意してください)。ほとんどの場合、全体の実行時間は 1 秒未満に短縮されました。つまり、最後のチェックサットは大幅に高速化されました。

詳細を提供するために、Z3 のすべてのスコープ (低速、8 秒) の実行と、 でマークされたスコープ[XXX]がコメントされた Z3 の実行 (高速、0.3 秒) を比較しました。結果はこの差分で確認できます(左が遅い、右が速い)。

diff は、すべての check-sats が同じように動作することを示しています (「unsat」を echo することでコメント付きのものを偽造しました)。このことから、コメント付きのスコープは証明検索に影響しますが、最終的な結果には影響しないと結論付けています。

また、得られた統計の違いをある程度理解しようとしましたが、統計を正しく解釈する方法についてはほとんど知りません。ここに私が理解できるいくつかの統計があります：

• grobner(383 対 36) およびnonlinear-horner(342 対 25) であるため、実行が遅いほど算術関連の操作が多く実行されるようです。コメントされたスコープは確かに非線形算術に近づきます（そして他の多くの場合もそうです）が、コメントされたスコープの特定の証明は「自明」である必要がx != 0ありxます0 < x。

• memory(40 対 7)、これは、Z3 が低速バージョンのプログラムでより大きな探索空間を探索していることを示していると解釈します。

• quant-instantiations(43k 対 51k)、これは私を驚かせました。実行が大幅に高速であるにも関わらず、より多くの量指定子のインスタンス化がトリガーされたからです。

3SAT に関する次の問題を解決したかったのです。「TWICE-3SAT 入力: NP 困難であり、充足可能な割り当てが複数あることを示す方法」

私は、CBMC (C 境界モデル チェッカー) で「正確に 1 回」のプロパティを記述するためのより良い解決策を思いつくために一生懸命努力しています。つまり、行内の 1 つの要素の位置が値 1 (またはブール値 true としてチェックできる任意の正の数) を持つ必要があり、残りはすべてゼロでなければなりません。

M = 4 の場合

それ以上のMは大問題です。M = 8 としましょう。次のようなことをしなければなりません:

違反を 1 回だけチェックするのは簡単ですが、それを述べるのは簡単ではありません。もう 1 つのオプションがあります。2 次元配列の問題を 1 次元のビットベクトルの問題に記述してから、スマート xor を実行することです。しかし、私は現在それについて確信が持てません。

誰にも問題のより良い解決策がありますか?

理論的/実際的な問題があり、管理方法については今のところ手がかりがありません。

私は、遺伝学アルゴリズムを使用して、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