找到满足某些条件的 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 的第 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 求解器或二元决策图完成，我使用了 this website，它在内部使用了 BDD。

Answer 2

这是一个使用 SWI-Prolog 的 library(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

Answer 3

这是我在 Picat 中使用约束编程的实验性按位模块 (http://hakank.org/picat/bitwise.pi) 的实现。在我的机器上花了 0.007 秒。模型也在这里：http://hakank.org/picat/bit_patterns.pi

import bitwise.
import cp.

main => go.

go ?=>
   Size = 16,
   Type = unsigned,

   println("Answers should be:"),
   println([x = 0x4121, y = 0x48ab]),
   println(z=[0x1307, 0x1387, 0x1707, 0x1787]),
   nl,

   X = bitvar2(Size,Type),
   Y = bitvar2(Size,Type),
   Z = bitvar2(Size,Type),

   % Y \/ X = 0x49ab,
   Y.bor(X).v #= 0x49ab,

   % (Y >> 2) ^ X = 0x530b,
   Y.right_shift(2).bxor(X).v #= 0x530b,

   % (Z >> 1) /\ Y = 0x0883,
   Z.right_shift(1).band(Y).v #= 0x0883,

   % (X << 2) \/ Z = 0x1787,
   X.left_shift(2).bor(Z).v #= 0x1787,

   Vars = [X.get_av,Y.get_av,Z.get_av],
   println(solve),
   solve(Vars),

   println(dec=[x=X.v,y=Y.v,z=Z.v]),
   println(hex=[x=X.v.to_hex_string,y=Y.v.to_hex_string,z=Z.v.to_hex_string]),
   println(bin=[x=X.v.to_binary_string,y=Y.v.to_binary_string,z=Z.v.to_binary_string]),  
   nl,
   fail,
   nl.
go => true.

输出：

Answers should be:
[x = 16673,y = 18603]
z = [4871,4999,5895,6023]

dec = [x = 16673,y = 18603,z = 4871]
hex = [x = 4121,y = 48AB,z = 1307]
bin = [x = 100000100100001,y = 100100010101011,z = 1001100000111]

dec = [x = 16673,y = 18603,z = 4999]
hex = [x = 4121,y = 48AB,z = 1387]
bin = [x = 100000100100001,y = 100100010101011,z = 1001110000111]

dec = [x = 16673,y = 18603,z = 5895]
hex = [x = 4121,y = 48AB,z = 1707]
bin = [x = 100000100100001,y = 100100010101011,z = 1011100000111]

dec = [x = 16673,y = 18603,z = 6023]
hex = [x = 4121,y = 48AB,z = 1787]
bin = [x = 100000100100001,y = 100100010101011,z = 1011110000111]

Answer 4

但是，对于进行此类位计算，z3 (https://github.com/Z3Prover/z3) 可能是要走的路，无论是在建模还是功能方面：它可以处理任意长尺寸等。

这是一个使用 Python 接口的 z3 模型（也在这里：http://hakank.org/z3/bit_patterns.py）：

from z3 import *

solver = Solver()
x = BitVec('x', 16)
y = BitVec('y', 16)
z = BitVec('z', 16)

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

num_solutions = 0
print("check:", solver.check())
while solver.check() == sat:
    num_solutions += 1
    m = solver.model()

    xval = m.eval(x)
    yval = m.eval(y)
    zval = m.eval(z)
    print([xval,yval,zval])
    solver.add(Or([x!=xval,y!=yval,z!=zval]))

print("num_solutions:", num_solutions)

输出：

[16673, 18603, 4871]
[16673, 18603, 4999]
[16673, 18603, 6023]
[16673, 18603, 5895]
num_solutions: 4

Answer 5

使用 BDD 和位向量的 Python 解决方案，带有包 omega：

"""Solve a problem of bitwise arithmetic using binary decision diagrams."""
import pprint

from omega.symbolic import temporal as trl


def solve(values):
    """Encode and solve the problem."""
    aut = trl.Automaton()
    bit_width = 16
    max_value = 2**bit_width - 1
    dom = (0, max_value)  # range of integer values 0..max_value
    aut.declare_constants(x=dom, y=dom, z=dom)
        # declares in the BDD manager bits x_0, x_1, ..., x_15, etc.
        # the declarations can be read with:
        #     `print(aut.vars)`
    # prepare values
    bitvalues = [int_to_bitvalues(v, 16) for v in values]
    bitvalues = [reversed(b) for b in bitvalues]
    # Below we encode each bitwise operator and shifts by directly mentioning
    # the bits that encode the declared integer-valued variables.
    #
    # form first conjunct
    conjunct_1 = r' /\ '.join(
        rf'((x_{i} \/ y_{i}) <=> {to_boolean(b)})'
        for (i, b) in enumerate(bitvalues[0]))
    # form second conjunct
    c = list()
    for i, b in enumerate(bitvalues[1]):
        # right shift by 2
        if i < 14:
            e = f'y_{i + 2}'
        else:
            e = 'FALSE'
        s = f'((~ ({e} <=> x_{i})) <=> {to_boolean(b)})'
            # The TLA+ operator /= means "not equal to",
            # and for 0, 1 has the same effect as using ^ in `omega`
        c.append(s)
    conjunct_2 = '/\\'.join(c)
    # form third conjunct
    c = list()
    for i, b in enumerate(bitvalues[2]):
        # right shift by 1
        if i < 15:
            e = f'z_{i + 1}'
        else:
            e = 'FALSE'
        s = rf'(({e} /\ y_{i}) <=> {to_boolean(b)})'
        c.append(s)
    conjunct_3 = r' /\ '.join(c)
    # form fourth conjunct
    c = list()
    for i, b in enumerate(bitvalues[3]):
        # left shift by 2
        if i > 1:
            e = f'x_{i - 2}'
        else:
            e = 'FALSE'
        s = rf'(({e} \/ z_{i}) <=> {to_boolean(b)})'
        c.append(s)
    conjunct_4 = '/\\'.join(c)
    # conjoin formulas to form problem description
    formula = r' /\ '.join(
        f'({u})'
        for u in [conjunct_1, conjunct_2, conjunct_3, conjunct_4])
    print(formula)
    # create a BDD `u` that represents the formula
    u = aut.add_expr(formula)
    care_vars = {'x', 'y', 'z'}
    # count and enumerate the satisfying assignments of `u` (solutions)
    n_solutions = aut.count(u, care_vars=care_vars)
    solutions = list(aut.pick_iter(u, care_vars=care_vars))
    print(f'{n_solutions} solutions:')
    pprint.pprint(solutions)


def to_boolean(x):
    "Return BOOLEAN constant that corresponds to `x`."""
    if x == '0':
        return 'FALSE'
    elif x == '1':
        return 'TRUE'
    else:
        raise ValueError(x)


def int_to_bitvalues(x, bitwidth):
    """Return bitstring of `bitwidth` that corresponds to `x`.

    @type x: `int`
    @type bitwidth: `int`

    Reference
    =========

    This computation is from the module `omega.logic.bitvector`, specifically:
    https://github.com/tulip-control/omega/blob/
        0627e6d0cd15b7c42a8c53d0bb3cfa58df9c30f1/omega/logic/bitvector.py#L1159
    """
    assert bitwidth > 0, bitwidth
    return bin(x).lstrip('-0b').zfill(bitwidth)


if __name__ == '__main__':
    values = [0x49ab, 0x530b, 0x0883, 0x1787]
    solve(values)

输出给出了解决方案：

4 solutions:
[{'x': 16673, 'y': 18603, 'z': 4871},
 {'x': 16673, 'y': 18603, 'z': 4999},
 {'x': 16673, 'y': 18603, 'z': 5895},
 {'x': 16673, 'y': 18603, 'z': 6023}]

同意此处发布的其他答案。

可以使用pip从PyPI安装包omega，如下所示：

pip install omega

输出还包括编码问题的TLA+ 公式：

(((x_0 \/ y_0) <=> TRUE) /\ ((x_1 \/ y_1) <=> TRUE) /\ ((x_2 \/ y_2) <=> FALSE) /\ ((x_3 \/ y_3) <=> TRUE) /\ ((x_4 \/ y_4) <=> FALSE) /\ ((x_5 \/ y_5) <=> TRUE) /\ ((x_6 \/ y_6) <=> FALSE) /\ ((x_7 \/ y_7) <=> TRUE) /\ ((x_8 \/ y_8) <=> TRUE) /\ ((x_9 \/ y_9) <=> FALSE) /\ ((x_10 \/ y_10) <=> FALSE) /\ ((x_11 \/ y_11) <=> TRUE) /\ ((x_12 \/ y_12) <=> FALSE) /\ ((x_13 \/ y_13) <=> FALSE) /\ ((x_14 \/ y_14) <=> TRUE) /\ ((x_15 \/ y_15) <=> FALSE)) /\ (((~ (y_2 <=> x_0)) <=> TRUE)/\((~ (y_3 <=> x_1)) <=> TRUE)/\((~ (y_4 <=> x_2)) <=> FALSE)/\((~ (y_5 <=> x_3)) <=> TRUE)/\((~ (y_6 <=> x_4)) <=> FALSE)/\((~ (y_7 <=> x_5)) <=> FALSE)/\((~ (y_8 <=> x_6)) <=> FALSE)/\((~ (y_9 <=> x_7)) <=> FALSE)/\((~ (y_10 <=> x_8)) <=> TRUE)/\((~ (y_11 <=> x_9)) <=> TRUE)/\((~ (y_12 <=> x_10)) <=> FALSE)/\((~ (y_13 <=> x_11)) <=> FALSE)/\((~ (y_14 <=> x_12)) <=> TRUE)/\((~ (y_15 <=> x_13)) <=> FALSE)/\((~ (FALSE <=> x_14)) <=> TRUE)/\((~ (FALSE <=> x_15)) <=> FALSE)) /\ (((z_1 /\ y_0) <=> TRUE) /\ ((z_2 /\ y_1) <=> TRUE) /\ ((z_3 /\ y_2) <=> FALSE) /\ ((z_4 /\ y_3) <=> FALSE) /\ ((z_5 /\ y_4) <=> FALSE) /\ ((z_6 /\ y_5) <=> FALSE) /\ ((z_7 /\ y_6) <=> FALSE) /\ ((z_8 /\ y_7) <=> TRUE) /\ ((z_9 /\ y_8) <=> FALSE) /\ ((z_10 /\ y_9) <=> FALSE) /\ ((z_11 /\ y_10) <=> FALSE) /\ ((z_12 /\ y_11) <=> TRUE) /\ ((z_13 /\ y_12) <=> FALSE) /\ ((z_14 /\ y_13) <=> FALSE) /\ ((z_15 /\ y_14) <=> FALSE) /\ ((FALSE /\ y_15) <=> FALSE)) /\ (((FALSE \/ z_0) <=> TRUE)/\((FALSE \/ z_1) <=> TRUE)/\((x_0 \/ z_2) <=> TRUE)/\((x_1 \/ z_3) <=> FALSE)/\((x_2 \/ z_4) <=> FALSE)/\((x_3 \/ z_5) <=> FALSE)/\((x_4 \/ z_6) <=> FALSE)/\((x_5 \/ z_7) <=> TRUE)/\((x_6 \/ z_8) <=> TRUE)/\((x_7 \/ z_9) <=> TRUE)/\((x_8 \/ z_10) <=> TRUE)/\((x_9 \/ z_11) <=> FALSE)/\((x_10 \/ z_12) <=> TRUE)/\((x_11 \/ z_13) <=> FALSE)/\((x_12 \/ z_14) <=> FALSE)/\((x_13 \/ z_15) <=> FALSE))