sympy 求解线性方程 XOR, NOT
sympy solve linear equations XOR, NOT
我有 60 个方程和 70 个变量。
所有这些都在一个列表中：
(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 个方程和 70 个变量。 所有这些都在一个列表中：
(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，但请注意，在一般情况下，解决方案的数量呈指数增长。