私はsat4jソルバーに全く慣れていません..

一部のcnfファイルを入力として指定する必要があると書かれています

ルールを入力として与え、それが満足できるかどうかを取得する方法はありますか?

私のルールは次のようなものになります：

sat4jソルバーを使用してこれを解決する方法を教えてもらえますか?

SAT4Jを使用して以下の問題を解決しようとしています。私の質問は、API を使用して SAT4J に問題を指定する方法です。

問題は次のとおりです。

そのような：

SAT ソルバー SAT4J を使用して、部分加重最大充足可能性問題を解こうとしています。

私の .wcnf ファイルは大きく、約 100 万の制約が含まれています。

ソルバーを実行すると、出力の一部として次のようになります(OutOfMemoryError : Java heap space) :

つまり、ヒープ領域不足エラーです。ヒープ領域のサイズを増やすにはどうすればよいですか?また、それを増やすのに適した値は何ですか?

これは、制約ファイル Constraints.wcnf で sat4j ソルバーを呼び出す方法です。

/usr/bin/java -jar sat4j-maxsat.jar constraints.wcnf

ありがとう

何が起こるのですか：

次のコマンドを実行します。

ウィンドウが開かず、-remote フラグがない場合と同じコンソール出力が表示されます。

期待されること:

readme.txt から:

オンザフライ構成で sat4j を実行するには:

これらの手順により、Remote Control という名前の Java ウィンドウが開きます。Java コマンドのバージョン 1.5 がパスにあると仮定します。そうでない場合は、java コマンドへの完全なパスを指定するか、Java 2 SDK のインストール手順の説明に従って PATH 環境変数を更新する必要があります。

その他の詳細

2.3.4までの複数のバージョンのライブラリを試しました。

私のシステムは、Gnome 2 を搭載した Debian 7 です。

私のデフォルトの Java インストールは OpenJDK 1.7.0_65 です。

私のセカンダリJavaインストールはOracle Java 1.8.0_45です（同じ問題があります）。

gnuplot 4.6 がインストールされています。

私の最初のマシンには、2GB の RAM を備えた 32 ビットのデュアルコア CPU が搭載されています。

私の 2 番目のマシンには、8 GB の RAM を備えた 64 ビットのクアッド コア CPU が搭載されており、ソフトウェアはほぼ同じです。

質問

SAT4J のリモート コントロール機能を使用したことのある人はいますか? 私の方法の問題は何ですか？

アップデート

別のマシン (64 ビット Debian 7) では、ウィンドウが開きます。start dat ファイルは作成されますが、プロットは開始されません。

更新 2

生成されinstance.dimacs-gnuplot.gnuplotたファイルを gnuplot ターミナルから手動で実行したところunknown or ambiguous terminal type、x11タイプのメッセージが表示されました。パッケージをインストールしたgnuplot-x11ところ、職場のマシンで動作するようになりました。ダイアグラムが表示されます (すごい!)。残念ながら、自宅のマシンではまだリモート コントロール ウィンドウが開きません。

私は sat4j ソルバーがまったく初めてで、ブール値の満足可能な問題を研究しています。そして私は立ち往生しています。ブール式の整数変数を解くプログラムを作りたいです。

x1 < x2 + x3 ユーザーがその数式を入力すると、私のプログラムは x1 = 5 、 x2 = 3 、 x3 = 4 のようにこの数式を満たします (true を返します)。したがって、数式は true を返し、ユーザーは数式を満たすこの整数値を取得します。私はJavaでEclipseで作業しているため、sat4jで作成することは可能です。

学校のプロジェクトで N*N Queen 配置問題ソルバーを構築しようとしています。CNFステートメントを生成するプログラムを作成しました。「SAT4J埋め込みソルバー」7ページ目 3.1に引数としてそのアドレスを渡そうとしましたが、ParseFormatExceptionがスローされ続けます。また、stackoverflow で見つけたこのテキスト ファイルを使用しようとしました。

運もありません。私が編集したのは例外の catch ブロックだけなので、それがどれであるかがわかります。IntelliJ Idea Community エディションの Alt+Shift+F10 設定メニューから引数を与えようとしています。

誰かが私を助けてくれますか/私を案内してくれますか? 他の誰かのコードを使用するのはこれが初めてです + チュートリアルと呼ばれるものはありません。

多分、あなたは私に別の方法を提案することができます. この問題を解決して出力を得るには、SATソルバーが必要なだけなので、それを取得してチェス盤のグラフィカル表現を作成できます:)

現在のクラスコード。

私の理解では、インクリメンタル SAT 解法は、互いに非常に近いさまざまなモデルを評価するのに役立ちます。

これを使用してモデルを評価し、後で変更した場合は、以前のソリューションを使用して再評価し、より迅速な結果を得たいと考えています。しかし、さまざまな SAT ソルバー (Sat4J、Minisat、mathsat5) を調べたところ、すべてのモデルが 1 回の実行で提示された場合にのみ、漸進的に解決できるようです。

私はSATの解決にかなり慣れていないので、何かを見落としているかもしれません。後で使用するために解決インスタンスを保存する方法はありませんか? インスタンスを閉じると、すべての学習が失われますか?

Sat4j ライブラリを使い始めたばかりです。特定の CNF 入力を解析して単純化するのにかかる時間を計算する方法を教えてください。

利用した

リーダーが解析して isSatisfiable にかかる時間を計算したいと思います。可能であれば、 sat4j lib を使用して収集しようとしている詳細のスクリーンショットを処理したすべての cnf ファイルの画像内の情報を見つけるように親切に指示して ください。