Python中的XOR线性方程组求解器

Question

我有n行n+1列的矩阵，需要构建这样的系统例如矩阵是

x4 x3 x2 x1 result
1  1  0  1  0
1  0  1  0  1
0  1  0  1  1
1  0  1  1  0

则方程为(+为XOR(

x4+x3+x1=0
x4+x2=1
x3+x1=1
x4+x2+x1=0

我需要以x1的列表形式返回答案，。。。。。我们如何在python中做到这一点？

Answer 1

您可以使用微软Z3求解器的Python接口pyz3：

from z3 import *
def xor2(a, b):
return Xor(a, b)
def xor3(a, b, c):
return Xor(a, Xor(b, c))
#  define Boolean variables
x1 = Bool('x1')
x2 = Bool('x2')
x3 = Bool('x3')
x4 = Bool('x4')
s = Solver()
#  every equation is expressed as one constraint
s.add(Not(xor3(x4, x3, x1)))
s.add(xor2(x4, x2))
s.add(xor2(x3, x1))
s.add(Not(xor3(x4, x2, x1)))
#  solve and output results
print(s.check())
print(s.model())

结果：

sat
[x3 = False, x2 = False, x1 = True, x4 = True]

您可以将软件包安装为：

python -m pip install z3-solver

---

替代解决方案

您还可以使用SAT求解器cryptominisat的Python包装器。该求解器具有解决xor子句系统的内置功能。注释解释了如何安装必要的Python包pycryptosat
要解决的问题表示为变量列表和xor结果的数组。当然还有更优雅的方法来存储这些问题
解算器返回一个(可能很长(真值元组，每个变量一个。

#
#  How to install pycryptosat, the python wrapper of cryptominisat?
#  ================================================================
#  For Windows:
#  Download pycryptosat binary .whl from
#  https://www.lfd.uci.edu/~gohlke/pythonlibs/#pycryptosat
#  Python38Scripts>pip install pycryptosat-0.6.1.1-cp38-cp38-win_amd64.whl
#
#  Note: It is essential that the downloaded wheel file fits your installed ptyhon version
#        In my case cp38 for python 3.8 and 64 bits.
#        Otherwise, the pip install will abort with failure
#
#  For Unix, a simple "pip install pycroptosat" should suffice
import pycryptosat
from pycryptosat import Solver 
s = Solver(threads=1)
var_names = ["x4", "x3", "x2", "x1"]
var_id = [4, 3, 2, 1]
dic_id_name = {id: var_names[index] for index, id in enumerate(var_id)}
problem = [
#  x4 x3 x2 x1 result
[[1, 1, 0, 1], 0],
[[1, 0, 1, 0], 1],
[[0, 1, 0, 1], 1],
[[1, 0, 1, 1], 0]
]
#  Translate problem into set of xor clauses
for xor in problem:
clause = [var_id[index] for index, value in enumerate(xor[0]) if value == 1]
rhs = (xor[1] == 1)
#  add_xor_clause() expects a list of variable IDs as first parameter.
#  Second parameter is the right-hand-side of the xor expression.
#  print(f"xor clause {clause} {rhs}")
s.add_xor_clause(clause, rhs)
sat, solution = s.solve()

print(f"sat: {sat}")
if (sat):
print(f"solution:")
for id, name in sorted(dic_id_name.items(), key=lambda x:x[1]):
print(f"{name} = {solution[id]}")
else:
print("No solution. Sorry!")

结果输出：

sat: True
solution:
x1 = True
x2 = False
x3 = False
x4 = True

Answer 2

学习高斯，也可以用于XOR。然后编写一个高斯python程序