私は疑似ブールの問題があり、私はsat4jで解決する必要があります。sat4jについて、擬似ブール問題を解決するためにsat4jを使用する方法は？
誰かが私を助けることができますか？
F、A、B、C、D、E及びIは、によって表される値のリストを持っている：
私は名前の変数のリストを持っている：ここでは
は私の問題だ＃ 1、＃2、＃3 .....hは（＃1）
に＃1を割り当てる手段Iは、いくつかの例cを有しますonstraints：
h(a,#1)=1
h(a,#1)+h(b,#1)+h(c,#1)=1
h(a,#1)+h(a,#5)>=1
h(b,#2)+h(b,#3)+h(b,#4)>=1
上記の例のように多くの制約があります。 最後に、どの値をどの値に割り当てるかの結果が必要です。
どうすればsat4Jで解決できますか？制約をどのように表しますか？
私は擬似ブール充足問題として正しく問題を理解していれば、あなたは直接OPB fileとしてそれをエンコードすることができます：私は任意x1としてh(a,#1)エンコードされている
* #variable= 7 #constraint= 4
1 x1 = 1;
1 x1 1 x2 1 x3 = 1;
1 x1 1 x4 >= 1;
1 x5 1 x6 1 x7 >= 1;
、x2としてh(b,#1)、h(c,#1)をとしてh(a,#5)をx4,h(b,#2)をx5,h(b,#3)をx6,h(b,#4)をx7とする。 （
が続いて出力
java -jar org.sat4j.pb.jar yourfile.opb
を実行します（あなたは。各変数は1つの値のために最大で1つの値、または=を持っていることを示す
-1 x1 -1 x4 >= -1;
-1 x2 -1 x5 -1 x6 -1 x7 >= -1;
のような制約を追加することを望むかもしれない）を無視しますcで始まる多くのコメント行）：
s [email protected] You don’t need to manually build adders and comparators to use a pseudo-boolean solver like `org.sat4j.pb`.BLE
v x1 -x2 -x3 -x4 x5 -x6 -x7
の意味はx1とx5であり、x2,,x4,x6、およびx7はfalseです。
（私はorg.sat4j.pb Java APIを使用して同じことを行う方法があります確信している、おそらくこのコマンドラインレシピは、あなたがそれを把握するのに役立つ出発点を与える。）
私は使用しませんCNFソルバー。 SMTははるかに良いフィット感です。 –
どのようなSMTソルバーですか？私に1つお勧めできますか？私は私のJavaプロジェクトとコードを統合する必要があるので、私はpesudoブール問題を解決し、Java APIを提供するツールが必要です。 – JulieZhu
Z3は私がレクリエーション的に使ってきたポピュラーなSMTソルバです。私はそれを話すためにJavaを使用しようとしなかったが、他の人は、少なくともGoogleによると。Z3のシンプルなLISPy I/O構文は、どのような場合でも解析するのが難しくありません。 –