Microsoft Solver Foundation SAT CNF

Question

Я пытаюсь использовать Microsoft Solver Foundation SatSolver для решения простой проблемы CNF через Visual Studio (C# или VB). Может ли кто-нибудь опубликовать простой пример, объясняющий, как это можно сделать?

Вот короткий пример:

 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.

Благодаря Guy

Answer 1

Вы должны использовать s1.Not(t1) вместо s1.Neg(t1).