布尔方程组

Question

我正在研究求解布尔方程组。具体来说，我试图找到位向量 S1...S3 和/或 C1...C3 的值，以便它们的 XOR 结果在下表中给出（以十六进制值表示）。有什么想法吗？

Answer 1

因此我们想要确定 6 个 32 位序列，总共 192 个未知的十六进制数字。我们可以只关注每个数字的第一个数字来说明我们如何尝试解决其他数字。

我们将S1、S2和S3的第一位数字分别称为a、b和c。我们也将 C1、C2 和 C3 的前几位分别称为 x、y 和 z。那么我们有以下等式，其中*代表异或：

a * x = E     b * x = A     c * x = 7
a * y = 2     b * y = 6     c * y = B
a * z = 1     b * z = 5     c * z = 8

让我们注意 XOR 的一些属性。首先，它是关联的。也就是说，A XOR (B XOR C) 始终等于 (A XOR B) XOR C。其次，它是可交换的。也就是说，A XOR B 始终等于 B XOR A。此外，对于任何 A，A XOR A 始终是“假”向量 (0)。XOR FALSE 始终是 A，其中 FALSE 代表“假”向量（0） ）。这些事实让我们可以用代数来求解变量并用代数来求解。我们可以先求解c，代入并简化得到：

a * x = E     b * x = A     z * x = F
a * y = 2     b * y = 6     z * y = 3
a * z = 1     b * z = 5     c = 8 * z

接下来我们可以做z：

a * x = E     b * x = A     y * x = C
a * y = 2     b * y = 6     z = 3 * y
a * y = 2     b * y = 6     c = 8 * z

我们发现我们的几个方程是多余的。我们预计系统不会不一致，因为我们有六个未知数的九个方程。让我们继续 y:

a * x = E     b * x = A     y = C * x
a * x = E     b * x = A     z = 3 * y
a * x = E     b * x = A     c = 8 * z

我们现在发现我们有更多无用的方程。但现在我们遇到了麻烦：我们只有五个不同的等式和六个未知数。这意味着我们的系统未指定，我们将有多种解决方案。我们可以选择一个或全部列出。让我们继续 x:

a * b = 4     x = b * A     y = C * x
a * b = 4     x = b * A     z = 3 * y
a * b = 4     x = b * A     c = 8 * z

这意味着方程 a * b = 4 的每个解都有一个解。有多少个解？嗯，必须有 16 个，每个 a 值对应一个。这是一个表格：

a: 0  1  2  3  4  5  6  7  8  9  A  B  C  D  E  F
b: 4  5  6  7  0  1  2  3  C  D  E  F  8  9  A  B

我们可以使用我们确定的其他方程来填写表格的其余部分。每行都将是一个解决方案。

您可以对十六进制序列中的 32 个位置中的每一个位置继续此过程。对于每个职位，您都会发现：

1. 有多种解决方案，正如我们在第一个位置找到的那样
2. 如果你最终得到六个有用的方程，就有一个独特的解决方案
3. 如果您发现其中一个方程在替换后变得矛盾（例如，A = 3），则无解。

如果发现一个位置无解，那么整个系统就无解。否则，您将得到许多解，这些解是 32 个位置中每个位置的非零解数的乘积。

Answer 2

MiniZinc 求解器来救援

使用MiniZinc作为约束求解器，我找到了以下解决方案：

S1 = 198BCC8B3008020C3086B4881C1D5100
S2 = 541DE11561A39900404F35599C8C150B
S3 = 84018896535D0F15C8528DE2B18821B2
C1 = FFDFFFFF7FFFFFFFFFDFBFFFBFFFF7BF
C2 = 3E2F8738BE0F87383E2FC7387E0F8F78
C3 = 00200000800000000020400040000840

如何获得MiniZinc模型

使用 C# 程序，我生成了具有 768 个布尔决策变量的 MiniZinc 模型。 该模型有 1158 行长，开头如下：

array[1..3, 1..128] of var bool: c;
array[1..3, 1..128] of var bool: s;

constraint s[1,1] == c[1,1];
constraint s[1,2] != c[1,2];
constraint s[1,3] != c[1,3];
constraint s[1,4] != c[1,4];

模型结束：

constraint s[3,124] != c[3,124];
constraint s[3,125] == c[3,125];
constraint s[3,126] != c[3,126];
constraint s[3,127] == c[3,127];
constraint s[3,128] == c[3,128];

MiniZinc 约束解释

可以解释/翻译这些限制：

由于“E6543...”中

E

的最低有效位为0，因此S1的第一位必须等于C1的第一位。
作为第二位，如果

E

为 1，则 S1 的第二位必须不等于 C1 的第二位。
等等

事后感想

事实上有多种解决方案。

求解器的求解运行时间远低于一秒。

我分析了在什么条件下问题才能得到解决。 九个约束位控制给定位置 0..127 的 C1、C2、C3、S1、S2、S3 的位位置。事实证明，并非所有

2**9 = 512

可能的位组合都会产生可解的星座。只有 32 个是可以解决的。

SAT 求解器作为替代方案

另一种选择是生成 CNF 输入到 SAT 求解器，如 CryptoMiniSat。每个相等/不等约束都可以编码在两个 CNF 子句中。这种方法需要

9 * 128 * 2 = 2304

子句和 768 个布尔变量。