我正试图使用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
您应该使用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;"。