問題タブ [satisfiability]

質問する

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

107 問題
Newest
Active
Bountied
318
Unanswered
0 投票する
2 に答える
171 参照

constraint-programming - SMT-Lib 標準は理論の組み合わせをサポートしていますか?

SMT における理論の組み合わせを扱おうとしている研究がいくつかあることは知っています。ただし、SMT-Lib 2.0 言語 ( http://smtlib.cs.uiowa.edu/docs.html ) は、この点に関して何も述べていません。私の質問は、それがサポートされているかどうかです。また、複数の理論を同時に処理する機能を提供するソルバーは何ですか?

ありがとう、

0 投票する
2 に答える
624 参照

graph-theory - 3-sat およびトゥッテ多項式

次の 3-SAT インスタンスと対応するグラフを検討してください。

ここに画像の説明を入力

グラフは他の2つの形式で表示できます

ここに画像の説明を入力

このグラフのトゥッテ多項式は

ここに画像の説明を入力

グラフの独立数が 4 の場合、考慮される 3-SAT インスタンスは充足可能です。この事実は、コードを使用してチェックされます。

対応する出力は次のとおりです。

対応するグラフの補数は

ここに画像の説明を入力

グラフの補数のトゥッテ多項式は

ここに画像の説明を入力

補数のクリーク数は 4 であり、考慮されている 3-SAT インスタンスは充足可能であると言えます。

問題は次のとおりです。トゥッテ多項式を使用して、考慮されている 3-SAT インスタンスが充足可能かどうかを判断できますか?

0 投票する
2 に答える
859 参照

algorithm - CSP/SAT に関する条項とは?

質問は次のとおりです。

スポーツ リーグのスケジューリング問題について、次のルールと定義を検討してください。

  • N (偶数) チームで、2 チームごとにシーズン中に 1 回だけ対戦します。
  • シーズンは (N-1) 週間続きます。
  • 各チームは、シーズンの各週に 1 試合を行います。
  • 1 週間に N/2 の期間またはスロットがあります。すべてのスロットが 1 つのゲームにスケジュールされています。

(a) (25 点) スポーツ リーグのスケジューリング問題をブール充足可能性問題としてエンコードします。ヒント：

  • 2 つの異なるチームが特定のスロットで互いにプレーすることをモデル化するには、各スロットを 2 つのサブスロットに分割します。毎週、N 個のサブスロットがあります。連続するサブスロット (奇数のサブスロットと偶数のサブスロットが続く) をプレイする 2 つのチームが実際に互いに対戦するという規則を採用します。
  • 変数 Xijk は、チーム i がサブスロット j で第 k 週にプレーする場合に True が割り当てられます。
  • 変数 Yijk は、チーム i がチーム j と k 週に対戦する場合に真が割り当てられます。

1 つの質問があります。各サブスロットで 1 つのチームがプレーするという条項を提示してください。条項はいくつありますか？

私の質問: ここでの「条項」とは実際にはどういう意味ですか? 私はこの質問を投稿して、誰かが質問が何を尋ねようとしているのか教えてくれることを願っています.私は直接的な解決策を探しているわけではありません.

誰かが助けてくれたらありがとう。

0 投票する
1 に答える
153 参照

algorithm - 多変量関数の機能を決定する SAT ソルバー?

ブール充足性問題は、ブール式の充足可能性をチェックするための一般化です。ここで、ブール式は多項式の非負アルゴリズムによって生成されます。多項式は、たとえば、変数の量がどこにあるか$x_1x_2+x_2x_3$など$x_1$、いくつかの間隔である可能性があります。現在、非負性などの多項式の機能を分枝限定アルゴリズムなどの特別なアルゴリズムを使用してチェックしています。このアルゴリズムでは、大きな問題を小さな問題にしますが、MiniSatなどの一部の SAT ソルバーで約束されている学習などの機能が欠けています。そう$x_i\in[0.1,0.3]\;\;\forall i=1,...,n$$n$

  1. 多項式関数や一般的な多変量関数などの多項式のプロパティをチェックするように設計された SAT ソルバーはありますか?

  2. 多変量関数と非負アルゴリズムをブール式に変換する簡単な方法はありますか?

0 投票する
2 に答える
2392 参照

haskell - Haskell: 高速でシンプルな SAT ソルバーへのバインド

今日は、Haskell での SAT 解決のオプションについても調べてみました。まず、ピコサット ソルバーへの独自のインターフェイスを作成することに取り組みました。

すると、 SBV ライブラリがあることがわかりました。Z3、Yices、CVC4、および Boolector へのインターフェイスです。

また、github で Google 検索を行ったところ、Picosatバインディングも利用できることがわかりました。

高速/高パフォーマンスの制約を考慮して、検討する価値のある SAT ソルバーへの haskell バインディングは他にありますか? Carification: 高パフォーマンスの SAT 解法に適しています (たとえば、数日間実行される問題や、2^20 以上の SAT 問題をチェックするので、できるだけ早く終了する必要がある問題など)。たとえば、ハックで特に欠けているのは、Plingeling のような高速な並列 SAT ソルバーへのバインドです。(また、github で現在更新されている picosat バインディングを偶然見つけたので、他のオプションを見逃す可能性が非常に高いです)

SBV ライブラリのデフォルト オプションは、Z3 SMT ソルバーです。picosat は Z3 よりも単純な SAT 解法で高速であるという私の知識に基づいた推測は正しいですか?


12345678910