哪种算法可以求解变量为位且运算为xor的方程组？

Question

我正在尝试解决方程组。每个等式的形式如下：

V1 xor V2 xor ... xor Vx = Sx

Vx和Sx是单比特变量。 Sx是已知的，我需要找到所有Vx的值

---

例如：

V1 xor V2 xor V3 = 1
V1 xor V2 = 0
V2 xor V3 = 1

（B1 = 0，B2 = 0，Bc = 1）

---

实际上，我有数千个变量（每个都是一个位）和数千个方程（只有xor运算）。我知道至少有一个解决方案，我只需要一个解决方案。

我知道如何为小型系统手动解决这个问题，但我不知道如何构建算法来解决这个问题。

你能帮帮我吗？我是一名开发人员，我理解如何使用位，xor运算符和数据结构，但我在数学方面经验不足，我不知道使用哪种方程式求​​解方法。我对矩阵运算也不是很直观，所以如果我需要它，请尝试解释它非常慢！ ：p

谢谢！

Answer 1

您可以使用高斯消除：https://en.wikipedia.org/wiki/Gaussian_elimination

对于采用模2的整数，XOR是加法（和减法 - 它是相同的），所以它很容易：

例如，找到包含v1的等式，并将其添加到包含v1的所有其他等式中以从中移除v1：

v1 XOR v2        = 1
      +
v1        XOR v3 = 0
--------------------
       v2 XOR v3 = 1

使用不同的方程从所有其他方程中移除v2，移除v3等不同的方程，直到所有方程只有一个变量。

Answer 2

我几乎把它放在另一个评论中，但它似乎是一个答案，所以在这里。

我担心你可能是SOL。例如，给定Sx为111，其中有一个矩阵

L1 = 100   | Sx(L1) = 1
L2 = 010   | Sx(l2) = 1
L3 = 001   | Sx(L3) = 1

还有2个等效矩阵适合解决方案（L3可以很容易为010或100）。

此外，给定Sx为001 - 即使您知道L1和L2在每个变量上的系数为0，您也不知道L3中的哪个Vx是“有效”位。

Answer 3

好的，要做到这一点，你需要了解一些关于xor和not以及0 = false和1 = true的代数规则。

首先，xor满足联想和交换法则。如果我们将xor放在一起，我们可以重新调整我们内心的内容。

接下来，x xor x = 0。当我们加上这个事实，0 xor y = y我们可以放弃匹配的变量对。

接下来，替换。 x1 xor x2 xor ... xor xn = 0形式的等式意味着x1 = x2 xor x3 xor ... xor xn。同样x1 xor x2 xor ... xor xn = 1暗示x1 = 1 xor x2 xor x3 xor ... xor xn。这些事实可以用你的其他方程代替。这可能会导致重复的变量，然后我们可以放弃。

这意味着每个方程都可以用来根据其他方程写出一个变量，然后可以将其替换为其他方程。现在这是一个因变量。最后，我们将有三个状态之一。

1. 1 = 0意味着没有解决方案。
2. 没有方程式，也没有变量。有一个解决方案。只需向后替换就可以了。
3. 几个变量从未被消除，但你已经超出了方程式。那些变量是免费的。您可以将它们设置为任何内容并获得答案。你不妨把它们设置为1。

让我用你的方程来说明。

(1) 1 = V1 xor V2 xor V3
(2) 0 = V1 xor V2
(3) 1 = V2 xor V3

从(1)我们知道：

(4) V1 = 1 xor V2 xor V3

（注意，V1被淘汰。）将(4)替换为(2)并且（3）获得：

(5) 0 = V1 xor V2
      = (1 xor V2 xor V3) xor V2
      = 1 xor V3

(6) 1 = V2 xor V3

（请注意，(6)是一个简单的替代。）

从(5)我们得到：

(7) 1 = V3

（注意，V3被淘汰。）将(7)替换为(6)，我们得到：

(8) 1 = V2 xor V3
      = V2 xor 1

从(8)我们得到：

(9) V2 = 1 xor 1 = 0

（注意，V2被淘汰。）

规则(9)，(7)和(4)淘汰了V2，V3和V1所以有一个解决方案。它是：

(9) V2 = 0
(7) V3 = 1
(4) V1 = 1 xor V2 xor V3 = 1 xor 0 xor 1 = 0

请注意，这是一个完全机械的过程。在每个步骤中，我采用了我离开的第一个等式，用它来编写一个变量，然后将其替换为其他变量。少一个等式，少一个变量。它总是有效的。

你必须为此制定一个好的表示和代码。但是知道你想要做什么将有希望帮助。

Answer 4

您可以使用MiniSAT算法。在Java中，它可以在LogicNG项目中获得。

您的示例可以在the SatisfiabilityInstances() function的Symja project中这样发布。在引擎盖下，LogicNG MiniSat.miniSat()被召唤。

SatisfiabilityInstances(Xor(v1,v2,v3)&&Not(Xor(v1,v2))&&Xor(v2,v3),{v1,v2,v3})

结果：

{{False,False,True}}