Choco Sat 공식

Question

Choco 4.0.1을 사용하여 SAT 공식을 모델링하려고합니다. 나는 docs을 읽고, 나는 javadoc에서 이해하려고 애 쓰고 있지만, 불행히도 나는 지금까지 실패하고있다. 이것은 처음으로 이러한 유형의 문제와 초코 작업을하는 것입니다. 그래서, 나는 아주 명백한 것을 요구하고 있을지도 모른다.

내가 좋아하는 모델에 제약의 번호를 추가해야합니다 (각 VAR는 BoolVar입니다) :

x <-> (a and -b) 

내가 모델에 방법을 ifOnlyIf 사용하는 것을 시도하고있다,하지만 나는 부정하는 방법을 모른다 변수 또는 사용 및. 누군가가 (이상적으로) 샘플 코드 나 이러한 유형의 제약 조건을 모델링하는 방법에 대한 아이디어를 저에게 제공 할 수 있습니까?

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

그러나, 설명서가 오래된 것 같다 :

Answer 1

는 Choco 4.0.1online manual에 따르면,이 같은해야한다. 내가 입력을 부정 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 
    } 
} 

:에 처럼이 코멘트에 제안, 나는 도착했다.