sat

2熱

1答えて

C++ライブラリとしてMiniSatを使用する場合、新しい変数はすべて、決定変数または非決定変数として作成できます。私が大まかに理解しているところは、ソルバーが分岐の際に次にどの変数を使用するかを決めるときに、非決定変数は考慮されないということです。しかし、私のプロジェクトでは、式が実際にはUNSATだったにもかかわらず、ソルバーがSATを返したときに、非決定変数が含意の左側にあるときに同等の関

0熱

1答えて

ScalaクラスのSATソルバを使用する

Scalaで書かれたアプリケーションから一般的なSATソルバを呼び出す必要があります。私はSAT4Jを見ていましたが、jarファイルとして簡単にインポートすることができますが、実際に使用することは困難です。 Scalaコード内からSAT問題を計算するためにSAT4j jarファイルを起動する方法はありますか？ SAT4Jが適切なアプローチではない場合、外部SATソルバーを起動する代わりに直接使用で

2熱

1答えて

C-SATとSATの違いは？

これらの2つのNP完全問題の違いは何ですか？ブール式を満たすことができるか（すなわち出力1）、一方は回路の文脈にあり、もう一方は単なる式であるかどうかを問われているように思える。しかし、ブール式回路からブール式を書くことはできませんでしたか？

-1熱

0答えて

SATベースの動作計画

SAT BASED MOTION PLANNING ALGORITHM シンプル運動計画問題は、問題を解決SATとして改造することができます。どのように誰がこれを可能に説明することができますか？この問題では、最初から最後まで衝突のないパスを見つける必要があります。

0熱

1答えて

パスを探す：SATを解く

私たちはn * mのグリッドを与えられています。このグリッドには、ボットの始点と終点のさまざまな場所に障害物があります。タスクは、最初から最後まで衝突のないパスを見つけることです。この問題は、SATの問題としてモデル化されます。この場合、最適な解決策を得るために何をすべきかを教えてください。

0熱

1答えて

SAT4J含意使用例

私はsat4jライブラリを初めて使用しています。たとえば、私は含意を定義することができます。 (A1 v A2 v A3) => (A1 ∧ A4) sat4jを使用して、すべての変数のブール値を見つけますか？私はsat4jの単体テストを見つけましたが、私は以下のようなものを試しました。問題は、hasASolution()がtrueを返しますが、solution変数が空であることです。 Depe

1熱

1答えて

DPLL一貫したリテラルセットとは何ですか？

私はSATソルバを書いています。私はDPLLアルゴリズムを実装し始めました。私はアルゴリズムとそれがどのように動作するのか理解していますが、私もそれを変形しましたが、私にとって気になるのは次のことです。 function DPLL(Φ) if Φ is a consistent set of literals then return true; if Φ conta

0熱

1答えて

リストを3SATフォームにフォーマットする

Pythonからしばらく離れていますので、フォーマットスキルは存在しません。このようなものに [[8, -6, -4], [-10, 4, 6], [6, -8, -9]] ： (x8 v ~x6 v ~x4)^(~x10 v x4 v x6)^(x6 v ~x8 v ~x9) 、その後、別の入力はTまたはFに任意のガイダンスを変更するよう各番号を参照することができ、この形式の何かを回すた

0熱

2答えて

SMT/SATソルバーとモデルチェッカー

最近、私は正式な検証技術を研究し始めました。文献では、モデルチェッカーとソルバーが何らかの意味で使用されています。しかし、モデルチェッカーとソルバーはどうつながっていますか？ p.s.いくつかの論文やリンクが提案されていれば幸いです。