找到满足某些条件的 16 位数字的最优雅的方法是什么？

Question

我需要找到所有 16 位数字 ( x, y, z) 的三元组（实际上只有在不同三元组中与相同位置的位完美匹配的位），这样

y | x = 0x49ab
(y >> 2) ^ x = 0x530b
(z >> 1) & y = 0x0883
(x << 2) | z = 0x1787

直接使用 8700K 的策略需要大约 2 天，这太多了（即使我会使用我可以访问的所有 PC（R5-3600、i3-2100、i7-8700K、R5-4500U、3xRPi4、RPi0/W）这将花费太多时间）。

如果位移位不在等式中，那么这样做将是微不足道的，但是使用位移位很难做同样的事情（甚至可能是不可能的）。

所以我想出了一个非常有趣的解决方案：将方程解析为关于数字位的语句（类似于“x XOR 的第 3 位 XOR y 的第 1 位等于 1”），并且所有这些语句都用 Prolog 语言之类的语言编写（或只是解释他们使用真值表操作）执行所有明确的位将被发现。这个解决方案也很困难：我不知道如何编写这样的解析器，也没有 Prolog 的经验。(*)

所以问题是：这样做的最佳方法是什么？如果是 (*) 那么怎么做呢？

编辑：为了更容易在此处编码数字的二进制模式：

0x49ab = 0b0100100110101011
0x530b = 0b0101001100001011
0x0883 = 0b0000100010000011
0x1787 = 0b0001011110000111

Answer 1

有四种解决方案。在所有这些中，x = 0x4121，y = 0x48ab。z 有四个选项（其中两个位可以自由为 0 或 1），即 0x1307、0x1387、0x1707、0x1787。

这可以通过将变量处理为 16 位数组并根据对布尔值的操作对它们进行按位运算来计算。这可能可以在 Prolog 中完成，也可以使用 SAT 求解器或二元决策图完成，我使用了这个在内部使用 BDD 的网站。

Answer 2

这是一个使用 SWI-Prologlibrary(clpb)解决布尔变量约束的方法（感谢 Markus Triska！）。

非常简单的翻译（我从未使用过这个库，但它相当简单）：

:- use_module(library(clpb)).

% sat(Expr) sets up a constraint over variables
% labeling(ListOfVariables) fixes 0,1 values for variables (several solutions possible)
% atomic_list_concat/3 builds the bitstrings

find(X,Y,Z) :-
    sat(
        *([~(X15 + Y15), % Y | X = 0X49ab (0100100110101011)
            (X14 + Y14),
           ~(X13 + Y13),
           ~(X12 + Y12),
            (X11 + Y11),
           ~(X10 + Y10),
           ~(X09 + Y09),
            (X08 + Y08),
            (X07 + Y07),
           ~(X06 + Y06),
            (X05 + Y05),
           ~(X04 + Y04),
            (X03 + Y03),
           ~(X02 + Y02),
            (X01 + Y01),
            (X00 + Y00),
           ~(0   # X15), % (Y >> 2) ^ X = 0X530b (0101001100001011)
            (0   # X14),
           ~(Y15 # X13),
            (Y14 # X12),
           ~(Y13 # X11),
           ~(Y12 # X10),
            (Y11 # X09),
            (Y10 # X08),
           ~(Y09 # X07),
           ~(Y08 # X06),
           ~(Y07 # X05),
           ~(Y06 # X04),
            (Y05 # X03),
           ~(Y04 # X02),
            (Y03 # X01),
            (Y02 # X00),
           ~(0   * Y15), % (Z >> 1) & Y = 0X0883 (0000100010000011)
           ~(Z15 * Y14),
           ~(Z14 * Y13),
           ~(Z13 * Y12),
            (Z12 * Y11),
           ~(Z11 * Y10),
           ~(Z10 * Y09),
           ~(Z09 * Y08),
            (Z08 * Y07),
           ~(Z07 * Y06),
           ~(Z06 * Y05),
           ~(Z05 * Y04),
           ~(Z04 * Y03),
           ~(Z03 * Y02),
            (Z02 * Y01),
            (Z01 * Y00),
           ~(X13 + Z15), % (X << 2) | Z = 0X1787 (0001011110000111)
           ~(X12 + Z14),
           ~(X11 + Z13),
            (X10 + Z12),
           ~(X09 + Z11),
            (X08 + Z10),
            (X07 + Z09),
            (X06 + Z08),
            (X05 + Z07),
           ~(X04 + Z06),
           ~(X03 + Z05),
           ~(X02 + Z04),
           ~(X01 + Z03),
            (X00 + Z02),
            (  0 + Z01),
            (  0 + Z00) ])),
    labeling([X15,X14,X13,X12,X11,X10,X09,X08,X07,X06,X05,X04,X03,X02,X01,X00,
              Y15,Y14,Y13,Y12,Y11,Y10,Y09,Y08,Y07,Y06,Y05,Y04,Y03,Y02,Y01,Y00,
              Z15,Z14,Z13,Z12,Z11,Z10,Z09,Z08,Z07,Z06,Z05,Z04,Z03,Z02,Z01,Z00]),
    atomic_list_concat([X15,X14,X13,X12,X11,X10,X09,X08,X07,X06,X05,X04,X03,X02,X01,X00],X),
    atomic_list_concat([Y15,Y14,Y13,Y12,Y11,Y10,Y09,Y08,Y07,Y06,Y05,Y04,Y03,Y02,Y01,Y00],Y),
    atomic_list_concat([Z15,Z14,Z13,Z12,Z11,Z10,Z09,Z08,Z07,Z06,Z05,Z04,Z03,Z02,Z01,Z00],Z).

我们在 0.007 秒内找到了几个解决方案，并添加了对十六进制（手动工作）的翻译：

?- find(X,Y,Z).
X = '0100000100100001',    %  4121
Y = '0100100010101011',    %  48AB
Z = '0001001100000111' ;   %  1307

X = '0100000100100001',    %  4121
Y = '0100100010101011',    %  48AB
Z = '0001001110000111' ;   %  1387

X = '0100000100100001',    %  4121
Y = '0100100010101011',    %  48AB
Z = '0001011100000111' ;   %  1707

X = '0100000100100001',    %  4121
Y = '0100100010101011',    %  48AB
Z = '0001011110000111'.    %  1787