Microsoft Solver Foundation SAT配置

Question

我正在尝试通过Visual Studio (C#或VB)使用Microsoft Solver Foundation SatSolver来解决一个简单的CNF问题。有人能贴出一个简单的例子来解释如何做到这一点吗？

下面是一个简短的示例：

        ConstraintSystem s1 = ConstraintSystem.CreateSolver();

        CspTerm t1 = s1.CreateBoolean("v1");
        CspTerm t2 = s1.CreateBoolean("v2");
        CspTerm t3 = s1.CreateBoolean("v3");
        CspTerm t4 = s1.CreateBoolean("v4");

        CspTerm tOr12 = s1.Or(s1.Neg(t1), s1.Neg(t2));
        CspTerm tOr13 = s1.Or(s1.Neg(t1), s1.Neg(t3));
        CspTerm tOr14 = s1.Or(s1.Neg(t1), s1.Neg(t4));

        CspTerm tOr23 = s1.Or(s1.Neg(t2), s1.Neg(t3));
        CspTerm tOr24 = s1.Or(s1.Neg(t2), s1.Neg(t4));

        CspTerm tOr34 = s1.Or(s1.Neg(t3), s1.Neg(t4));

        CspTerm tOr = s1.Or(t1, t2, t3, t4);

        s1.AddConstraints(tOr12);
        s1.AddConstraints(tOr13);
        s1.AddConstraints(tOr14);
        s1.AddConstraints(tOr23);
        s1.AddConstraints(tOr24);
        s1.AddConstraints(tOr34);
        s1.AddConstraints(tOr);

        ConstraintSolverSolution solution1 = s1.Solve();
        Console.WriteLine(solution1[t1]);
        Console.WriteLine(solution1[t2]);
        Console.WriteLine(solution1[t3]);
        Console.WriteLine(solution1[t4]);

结果应该只有一个值为1的变量，其余的应该是0，但是解决方案是1, 1，1,0。

谢谢，盖伊

Answer 1

您应该使用s1.Not(t1)而不是s1.Neg(t1)。