1

我正在尝试使用 Choco 4.0.1 对 SAT 公式进行建模。我阅读了文档，我试图从javadoc中理解，但不幸的是我到目前为止失败了。这是我第一次处理这些类型的问题，也是 choco。所以，我可能会问一些非常明显的问题。

我需要向模型添加一些约束，例如（每个 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 回答