Choco Sat 配方

Question

我正在尝试使用 Choco 4.0.1 为 SAT 公式建模。我读了 docs , I am trying to understand from the javadoc，但不幸的是我到目前为止都失败了。这是我第一次处理这类问题，也是 choco。所以，我可能会问一些非常明显的问题。

我需要向模型添加一些约束，例如（每个变量都是一个 BoolVar）：

x <-> (a and -b)

我正在尝试在模型中使用 ifOnlyIf 方法，但我不知道如何取反变量或使用 and。有人可以（理想情况下）为我提供一些示例代码或有关如何对这些类型的约束进行建模的任何想法吗？

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

但是，手册似乎已经过时了。就像评论中建议的那样，我到达了：

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() 来否定输入。

Choco Sat 配方

Choco Sat Formulation

constraint-programming

sat

choco