找到满足某些条件的 16 位数字的最优雅方法是什么？
What is the most elegant way to find 16-bit numbers which satisfy some conditions?
我需要找到所有 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 位异或 y 的第 1 位等于 1”），并将所有这些语句写在 Prolog 之类的东西中语言（或只是使用操作的真值表来解释它们）执行所有明确的位都会被发现。
这个解决方案也很难：我不知道如何编写这样的解析器，也没有使用 Prolog 的经验。 (*)
所以问题是：最好的方法是什么？如果是 (*) 那么该怎么做？
编辑：为了更容易在此处编码数字的二进制模式：
0x49ab = 0b0100100110101011
0x530b = 0b0101001100001011
0x0883 = 0b0000100010000011
0x1787 = 0b0001011110000111
有四种解法。在所有这些中，x = 0x4121，y = 0x48ab。 z有四个选项（它的两个位可以自由为0或1），即0x1307、0x1387、0x1707、0x1787。
这可以通过将变量视为 16 位数组并根据布尔运算对它们执行按位运算来计算。这可能可以在 Prolog 中完成，也可以使用 SAT 求解器或二进制决策图来完成，我使用了 this website，它在内部使用 BDD。
这是一个使用 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
这是我的实验性按位模块在 Picat 中的实现（http://hakank.org/picat/bitwise.pi ) using constraint programming. It took 0.007s on my machine. The model is also here: 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]
但是，对于进行此类位计算，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
使用 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}]
同意此处发布的其他答案。
软件包 omega 可以从 PyPI using pip 安装，如下所示：
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 位数字的三元组 (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 位异或 y 的第 1 位等于 1”），并将所有这些语句写在 Prolog 之类的东西中语言（或只是使用操作的真值表来解释它们）执行所有明确的位都会被发现。 这个解决方案也很难：我不知道如何编写这样的解析器，也没有使用 Prolog 的经验。 (*)
所以问题是：最好的方法是什么？如果是 (*) 那么该怎么做？
编辑：为了更容易在此处编码数字的二进制模式：
0x49ab = 0b0100100110101011
0x530b = 0b0101001100001011
0x0883 = 0b0000100010000011
0x1787 = 0b0001011110000111
有四种解法。在所有这些中，x = 0x4121，y = 0x48ab。 z有四个选项（它的两个位可以自由为0或1），即0x1307、0x1387、0x1707、0x1787。
这可以通过将变量视为 16 位数组并根据布尔运算对它们执行按位运算来计算。这可能可以在 Prolog 中完成，也可以使用 SAT 求解器或二进制决策图来完成，我使用了 this website，它在内部使用 BDD。
这是一个使用 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
这是我的实验性按位模块在 Picat 中的实现（http://hakank.org/picat/bitwise.pi ) using constraint programming. It took 0.007s on my machine. The model is also here: 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]
但是，对于进行此类位计算，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
使用 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}]
同意此处发布的其他答案。
软件包 omega 可以从 PyPI using pip 安装，如下所示：
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))