找到满足某些条件的 16 位数字的最优雅方法是啥？
Posted
技术标签:
【中文标题】找到满足某些条件的 16 位数字的最优雅方法是啥？【英文标题】：What is the most elegant way to find 16-bit numbers which satisfy some conditions?找到满足某些条件的 16 位数字的最优雅方法是什么？ 【发布时间】：2021-05-10 17:46:47 【问题描述】：我需要找到所有 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
【问题讨论】：
如果您可以将其转换为 3 x 16 布尔值上的合取范式命题句，那么您可以将其提供给 SAT solver。 【参考方案1】：有四种解决方案。在所有这些中，x = 0x4121，y = 0x48ab。 z 有四个选项（其中两个位可以为 0 或 1），分别为 0x1307、0x1387、0x1707、0x1787。
这可以通过将变量视为 16 位数组并根据布尔运算对它们执行按位运算来计算。这可能在 Prolog 中完成，也可以使用 SAT 求解器或二元决策图完成，我使用了 this website，它在内部使用了 BDD。
【讨论】：
"快速服务，保证解决方案"【参考方案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
【讨论】：
【参考方案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]
【讨论】：
【参考方案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
【讨论】：
【参考方案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))
【讨论】：
以上是关于找到满足某些条件的 16 位数字的最优雅方法是啥？的主要内容，如果未能解决你的问题，请参考以下文章
8-16位密码,数字、大小写字母组合、符号至少包含两种,是啥意思?
在 C 中存储和使用具有 1,000,000 位有效数字的浮点数的最有效方法是啥？
在 Silverlight 的 SaveFileDialog 中缺少 DefaultFileName 的最优雅的解决方法是啥？