Microsoft Solver Foundation SAT CNF

Я пытаюсь использовать 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.

Спасибо, парень


c# solver cnf
person Guy Shani    schedule 11.09.2014    source источник
comment
Компилятор VS делает это автоматически. Если что-то никогда не будет правдой, оно скажет вам...   -  person Scott Solmer    schedule 11.09.2014
comment
Можете ли вы привести небольшой пример?   -  person Guy Shani    schedule 12.09.2014
comment
i.stack.imgur.com/WjAF1.jpg   -  person Scott Solmer    schedule 12.09.2014
comment
Боюсь, вы не поняли мою проблему. Я не ищу способ определить, какие операторы if будут или не будут выполняться в моем коде. Мне нужно решить задачу SAT, определяемую как CNF.   -  person Guy Shani    schedule 14.09.2014
comment
Я предлагаю вам использовать MiniSat или picosat вместо этого решателя Microsoft. Они и проще в использовании, и имеют активное сообщество для поддержки (и часто задаваемые вопросы, примеры и т. д. в Интернете).   -  person Mate Soos    schedule 19.09.2014

Ответы (1)


arrow_upward
0
arrow_downward

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

person user2304591    schedule 12.08.2016