专业 SAT 求解器（？）

Question

（上下文）

给定两个长度为 16 的字节数组，例如

L

和

H

，可以通过以下方式定义从所有字节集合到自身的映射

M

。

如果

0 <= b < 256

是一个字节，则让

lo(b)

表示

b

的低 4 位，让

hi(b)

表示

b

的高 4 位。

令

L[i]

（分别为

H[i]

）表示

i

（分别为

L

）的第

H

个字节。还令

L[i, j]

（分别为

H[i, j]

）表示

j

（分别为

i

）的第

L

字节的第

H

位。

有了这一切，我们就可以定义

M(b) = L[lo(b)] & H[hi(b)]

。

其中

&

是按位与。

如果我们希望

M

满足

M(b) == m

形式的约束。然后必须相应地选择

L

和

H

（如果可能）。该约束相当于

L[lo(b)] & H[hi(b)] == m

。或者更准确地说是

L[lo(b), j] & H[hi(b), j] == m[j]

，其中

m[j]

是

j

的第

m

位。

一般来说，任何形式为

X & Y = Z

的方程，其中

X, Y, Z

是位（或布尔值），都等价于命题逻辑中的以下布尔子句：

~X | ~Y | Z
X | ~Z
Y | ~Z

其中

~X

是

X

的求反，

|

是按位或。

问题的最后一个问题是

m

 字节应该彼此不同（假设有多个约束）。如果两个字节中至少有一位不相等，则两个字节不相等。两个位 

X

 和 

Y

 不相等，当且仅当满足以下条款：

X | Y
~X | ~Y

因此这个问题可以使用3-SAT来解决。对此我有三个问题：

我的问题是否等价于 3-SAT，即任意 3-SAT 问题是否可以简化为它？还是可以进一步简化为不太困难的事情？
如果没有，您是否找到了有效解决该问题的算法？
如果是，那么“简单”的基于 CDCL 的求解器就足够了吗？ （我们正在处理大约 3000 个子句和 300 个变量）。

我已经尝试过基本的回溯求解器，但即使在几个小时后它也无法终止。我花了数周的时间思考这个问题，但未能想出专门的算法，然后才写下这篇文章。我当然可以使用现成的 SAT 求解器，但我有兴趣尽可能高效地解决这个问题。

提前谢谢您。

Answer 1

让我亲手做一下原题来说明这个问题的本质。

我将把字节 0x2C 作为半字节对 (2, C) 写入。如果我们考虑 1 位输出，那么对于每组半字节 S 和每组半字节 T，我们可以表达的函数是 S × T 的指示函数。原始论文为每个类分配一个单独的位：

{2} × {C} = {(2, C)}
{3} × {A} = {(3, A)}
{5, 7} × {B, D} = {(5, B), (5, D), (7, B), (7, D)}
{0} × {9, A, D} = {(0, 9), (0, A), (0, D)}
{2} × {0} = {(2, 0)}。

我省略了表中的值，因为它们并不重要。这指出了 SAT 公式的主要弱点：它是高度对称的，并且基本的分支策略会很困难。复杂的 SAT 求解器可以检测对称性并修剪冗余分支，但逻辑

很复杂，而且您真的不想为一个应用程序自己实现它。

我假设所有不属于任何类的字节都应该映射为 0。那么一个必要条件是每个类都可以表示为一个产品。如果类的数量最多与输出位一样多，那么这个条件也足够了，并且您不需要 SAT 求解器。否则，你就会遇到一个受限制的

测试覆盖问题。 我没有 NP 困难证明，但如果它不是 NP 困难，我会感到惊讶。