Microsoft Solver Foundation SAT CNF

本文关键字：CNF SAT Foundation Solver Microsoft | 更新日期: 2023-09-27 18:21:35

我正试图使用Microsoft Solver Foundation SatSolver通过Visual Studio（C#或VB）解决一个简单的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,0。

谢谢Guy

Microsoft Solver Foundation SAT CNF

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

请改用Microsoft.SolverFoundation.Solvers命名空间中的静态SatSolver.Solve函数：

SatSolverParams parameters = new SatSolverParams();//default
int limVar = 5; // highest literal + 1
//add terms that are used in your code
Literal[][] clauses = new Literal[][]
{
    //Literal is represented as an int value with boolean Sense
    new Literal[] { new Literal(1, false), new Literal(2, false) },   // Clause 1: !1 or !2
    new Literal[] { new Literal(1, false), new Literal(3, false) },   // Clause 2: !1 or !3
    new Literal[] { new Literal(1, false), new Literal(4, false) },   // Clause 3: !1 or !4
    new Literal[] { new Literal(2, false), new Literal(3, false) },   // Clause 4: !2 or !3
    new Literal[] { new Literal(2, false), new Literal(4, false) },   // Clause 5: !2 or !4
    new Literal[] { new Literal(3, false), new Literal(4, false) },   // Clause 6: !3 or !4
    new Literal[] { new Literal(1, true), new Literal(2, true), new Literal(3, true), new Literal(4, true) } // Clause 7: 1 or 2 or 3 or 4
};
IEnumerable<SatSolution> solutions = SatSolver.Solve(parameters, limVar, clauses);
foreach (SatSolution solution in solutions)
{
    bool[] evaluation = new bool[4];//boolean values of individual literals
    IEnumerable<Literal> lits = solution.Literals;
    foreach (Literal lit in lits)
    {
        //lit.Var is the int value that represents the literal
        //lit.Sense is either true or false, literal or his negation
        evaluation[lit.Var - 1] = lit.Sense;
    }
    Console.WriteLine($"Solution found: 1 = {evaluation[0]}, 2 = {evaluation[1]}, 3 = {evaluation[2]}, 4 = {evaluation[3]}");
}

正好有4种解决方案。每一个都有一个正的文字，其余的都是负的。不要忘记"使用Microsoft.SolverFoundation.Solvers；"。

相关文章：