CODEWITHSUNDEEP
c#solvercnf
Guy Shani
Guy Shani

Reputation: 21

Microsoft Solver Foundation SAT CNF

I am trying to use Microsoft Solver Foundation SatSolver to solve a simple CNF problem through Visual Studio (C# or VB). Can anyone post a simple example explaining how this can be done?

Here is a short example:

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

The result should have only one variable with a value of 1, and the rest should have 0, but the solution is 1,1,1,0.

Thanks Guy

Upvotes: 1

Views: 1506

Answers (2)

Damodar109
Damodar109

Reputation: 1

Use the static SatSolver.Solve function in Microsoft.SolverFoundation.Solvers namespace instead:

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]}");
}

There are exactly 4 solutions. Each has 1 positive literal and the rest are negative. Don't forget 'using Microsoft.SolverFoundation.Solvers;'.

Upvotes: 0

user2304591
user2304591

Reputation: 1

You should use s1.Not(t1) instead of s1.Neg(t1).

Upvotes: 0

Related Questions