1

Choco 4.0.1 を使用して SAT 数式をモデル化しようとしています。docsを読み、javadocから理解しようとしていますが、残念ながらこれまでのところ失敗しています。この種の問題とチョコに取り組むのはこれが初めてです。だから、私は非常に明白なことを尋ねているかもしれません。

モデルにいくつかの制約を追加する必要があります (各 var は BoolVar です):

x <-> (a and -b)

モデルで ifOnlyIf メソッドを使おうとしていますが、変数を否定する方法や and を使用する方法がわかりません。誰かが（理想的には）サンプルコードや、これらのタイプの制約をモデル化する方法に関するアイデアを提供してもらえますか?

4

1 に答える 1

2

Choco 4.0.1 オンラインマニュアルによると、次のようになります。

SatFactory.addClauses(LogOp.ifOnlyIf(x, LogOp.and(a, LogOp.nor(b))), model);
// with static import of LogOp
SatFactory.addClauses(ifOnlyIf(x, and(a, nor(b))), model);

ただし、説明書が古いようです。コメントで示唆されているように、私は次のようになりました：

import static org.chocosolver.solver.constraints.nary.cnf.LogOp.and;
import static org.chocosolver.solver.constraints.nary.cnf.LogOp.ifOnlyIf;
import static org.chocosolver.solver.constraints.nary.cnf.LogOp.nor;

import org.chocosolver.solver.Model;
import org.chocosolver.solver.variables.BoolVar;

public class AkChocoSatDemo {

    public static void main(String[] args) {
        // 1. Create a Model
        Model model = new Model("my first problem");

        // 2. Create variables
        BoolVar x = model.boolVar("X");
        BoolVar a = model.boolVar("A");
        BoolVar b = model.boolVar("B");

        // 3. Post constraints
        // LogOp omitted due to import static ...LogOp.*
        model.addClauses(ifOnlyIf(x, and(a, nor(b))));

        // 4. Solve the problem
        model.getSolver().solve();

        // 5. Print the solution
        System.out.println(x); // X = 1
        System.out.println(a); // A = 1
        System.out.println(b); // B = 0
    }
}

入力を無効にするためnor()に単一のパラメーターを使用しました。not()

于 2017-01-09T18:53:43.950 に答える