У меня есть 60 уравнений с 70 переменными. все они находятся в одном списке:sympy решать линейные уравнения XOR, NOT
(x0, x1, ..., x239) являются SymPy символы
list_a = [Xor(Not(x40), Not(x86)), Xor(x41, Not(x87)), ...]
и мой вопрос, если это возможно, каким-то образом преобразовать это уравнение к матричным или решили их. Я думаю, что у него может быть несколько решений.
Решение системы логических выражений такое же, как проверка SAT для конъюнкции (And) выражений.
In [3]: list_a = [Xor(Not(x40), Not(x86)), Xor(x41, Not(x87))]
In [4]: list_a
Out[4]: [¬x₄₀ ⊻ ¬x₈₆, x₄₁ ⊻ ¬x₈₇]
In [5]: satisfiable(And(*list_a))
Out[5]: {x87: False, x40: True, x86: False, x41: False}
Если вы хотите, чтобы все решения, которые вы можете пройти all_models=True, хотя отмечают, что в общем случае существует экспоненциально много решений.
Спасибо за решение, но если у меня 60 уравнений с 120 переменными, это занимает много времени. Есть ли возможность сделать это быстрее? –
Это зависит от того, какая часть идет медленно. Обычно это либо медленное преобразование в cnf, либо решение SAT. Вы можете проверить, выполнив 'to_cnf (And (* list_a))' для вашей системы отдельно. – asmeurer
Похоже, системы линейных уравнений на булевом пространстве решаются точно так же, как системы линейных уравнений на вещественных числах. Не могли бы вы пояснить в своем вопросе, ищете ли вы алгоритм или как реализовать алгоритм, который у вас уже есть, или и то, и другое? – Vovanrock2002
Звучит как проблема SAT. –
Я ищу как.Algorithm, так и для преобразования из списка в матрицу. –