Choco Sat定式化

Question

Choco 4.0.1を使用してSAT式をモデル化しようとしています。私はdocsを読んで、私はjavadocから理解しようとしていますが、残念ながら私はこれまで失敗しています。これは初めてのこれらのタイプの問題とチョコで働いています。だから、私は何かを非常に明白に求めているかもしれません。

私は（各varがBoolVarである）のようなモデルに制約の数を追加する必要が

：

x <-> (a and -b) 

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

Answer 1

Choco 4.0.1online manualによると、それはこのようなものでなければなりません：

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); 

しかし、マニュアルは古くなっているようです。私は入力を否定するnot()のような単一のパラメータでnor()を使用していた

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 
    } 
} 

： などはコメントで提案、私が到着しました。