問題タブ [sat]
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.
java - SAT4J 含意のユースケース
私はsat4jライブラリが初めてです。(A1 v A2 v A3) => (A1 ∧ A4)sat4j を使用して含意を定義し、すべての変数のブール値を見つけるにはどうすればよいですか?
以下のリストのようなものを試したよりも、sat4jの単体テストを見つけました。問題はhasASolution()true を返しますが、solution変数が空であることです。
prolog - BumbleBEE SAT ソルバーのコンパイル
http://amit.metodi.me/research/bee/から bumblebee sat-solver をコンパイルしようとしています。SWI-Prolog と MinGW を既にインストールしていますが、cmd に「make-minisat」と入力すると、次のようになります。
g++ がプロローグ ヘッダー ファイルに到達できないようです。何か案は？私はwin 10、64ビットで作業しています。
prolog - Prolog で Groebner Basis SAT ソルバーを作成する
Boolean Grobner Bases の実装を使用して、結合正規形 (CNF) から変換する SAT ソルバーを作成しようとしています。
a) 特定の変数の否定。たとえば、-xに変換され1+xます。
b) 同じ変数を追加すると、結果は 0 になりますx + x = 0。(XOR を使用する必要があります)。
c) 同じ変数を乗算すると、同じ変数になります。例えばx*x = x。
現時点では、入力は次のようにSATコンペティションのようにテキストファイルにある必要があるため、開始方法をまだ理解しようとしています。
ありがとう。
編集
sat - Yosys 命令「sat -dump_cnf」
Verilog にサンプルの組み合わせ回路があり、命令に従って論理合成を行い、blif ファイルを生成できます。
ただし、回路から CNF 式を生成する必要があります。ABC などのツールでは、組み合わせマイター (つまり、1 つの出力) からのみ生成できます。
yosys 命令「sat -dump_cnf FILE」を試してみたところ、実際に CNF ファイルを生成できました。ただし、CNF 内の変数を回路内の I/O にマップする方法がわかりません。
Yosys の "sat -dump_cnf" 機能を調べた人はいますか?