問題タブ [sat4j]

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.

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

java - SAT4J 含意のユースケース

私はsat4jライブラリが初めてです。(A1 v A2 v A3) => (A1 ∧ A4)sat4j を使用して含意を定義し、すべての変数のブール値を見つけるにはどうすればよいですか?

以下のリストのようなものを試したよりも、sat4jの単体テストを見つけました。問題はhasASolution()true を返しますが、solution変数が空であることです。

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

java - Sat4J/CNF における掃海艇の制約の表現

SAT ソルバー (sat4j) を使用してマインスイーパ ソルバーを実装しようとしていますが、それらがどのように機能するかを簡単に理解しています。x+y+Z+....=2しかし、SAT ソルバーはブール入力を使用するため、地雷の表現方法がわかりません。以下の表のようなもの:

a+b+c+f+g+i+j+k = 2と と書くことができますc+d+e+g+h+k+l+m= 3