如何解决找到满足某些条件的 16 位数字的最优雅的方法是什么？
我需要找到所有 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
解决方法
有四种解决方案。在所有这些中，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,X00],X),atomic_list_concat([Y15,Y00],Y),atomic_list_concat([Z15,Z00],Z).
我们在 0.007 秒内找到了几个解决方案，并添加了对十六进制（手动工作）的翻译：
?- find(X,Z).
X = '0100000100100001',% 4121
Y = '0100100010101011',% 48AB
Z = '0001001100000111' ; % 1307
X = '0100000100100001',% 48AB
Z = '0001001110000111' ; % 1387
X = '0100000100100001',% 48AB
Z = '0001011100000111' ; % 1707
X = '0100000100100001',% 48AB
Z = '0001011110000111'. % 1787
这是我的实验性按位模块 (http://hakank.org/picat/bitwise.pi) 在 Picat 中使用约束编程的实现。在我的机器上花了 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,Z = bitvar2(Size,% 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]),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,z = 4999]
hex = [x = 4121,z = 1387]
bin = [x = 100000100100001,z = 1001110000111]
dec = [x = 16673,z = 5895]
hex = [x = 4121,z = 1707]
bin = [x = 100000100100001,z = 1011100000111]
dec = [x = 16673,z = 6023]
hex = [x = 4121,z = 1787]
bin = [x = 100000100100001,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,4999]
[16673,6023]
[16673,5895]
num_solutions: 4
使用 BDD 和位向量的 Python 解决方案，包含 omega 包：
python3 -m modernize -w SConstruct
Loading the following fixers:
fissix.fixes.fix_apply (apply)
fissix.fixes.fix_except (except)
fissix.fixes.fix_exec (exec)
fissix.fixes.fix_execfile (execfile)
fissix.fixes.fix_exitfunc (exitfunc)
fissix.fixes.fix_funcattrs (funcattrs)
fissix.fixes.fix_has_key (has_key)
fissix.fixes.fix_idioms (idioms)
fissix.fixes.fix_long (long)
fissix.fixes.fix_methodattrs (methodattrs)
fissix.fixes.fix_ne (ne)
fissix.fixes.fix_numliterals (numliterals)
fissix.fixes.fix_operator (operator)
fissix.fixes.fix_paren (paren)
fissix.fixes.fix_reduce (reduce)
fissix.fixes.fix_renames (renames)
fissix.fixes.fix_repr (repr)
fissix.fixes.fix_set_literal (set_literal)
fissix.fixes.fix_standarderror (standarderror)
fissix.fixes.fix_sys_exc (sys_exc)
fissix.fixes.fix_throw (throw)
fissix.fixes.fix_tuple_params (tuple_params)
fissix.fixes.fix_types (types)
fissix.fixes.fix_ws_comma (ws_comma)
fissix.fixes.fix_xreadlines (xreadlines)
libmodernize.fixes.fix_basestring (basestring)
libmodernize.fixes.fix_dict_six (dict_six)
libmodernize.fixes.fix_file (file)
libmodernize.fixes.fix_filter (filter)
libmodernize.fixes.fix_import (import)
libmodernize.fixes.fix_imports_six (imports_six)
libmodernize.fixes.fix_input_six (input_six)
libmodernize.fixes.fix_int_long_tuple (int_long_tuple)
libmodernize.fixes.fix_itertools_imports_six (itertools_imports_six)
libmodernize.fixes.fix_itertools_six (itertools_six)
libmodernize.fixes.fix_map (map)
libmodernize.fixes.fix_metaclass (metaclass)
libmodernize.fixes.fix_next (next)
libmodernize.fixes.fix_print (print)
libmodernize.fixes.fix_raise (raise)
libmodernize.fixes.fix_raise_six (raise_six)
libmodernize.fixes.fix_unichr (unichr)
libmodernize.fixes.fix_unicode_type (unicode_type)
libmodernize.fixes.fix_urllib_six (urllib_six)
libmodernize.fixes.fix_xrange_six (xrange_six)
libmodernize.fixes.fix_zip (zip)
Applying the following explicit transformations:
(None)
RefactoringTool: Skipping optional fixer: idioms
RefactoringTool: Skipping optional fixer: set_literal
RefactoringTool: Skipping optional fixer: ws_comma
RefactoringTool: Refactored SConstruct
--- SConstruct (original)
+++ SConstruct (refactored)
@@ -38,6 +38,7 @@
"""
from __future__ import print_function
+from __future__ import absolute_import
from buildutils import *
if not COMMAND_LINE_TARGETS:
RefactoringTool: Files that were modified:
RefactoringTool: SConstruct
输出给出了解决方案：
(record.current_price === 'Timeout' && "red")同意此处发布的其他答案。
可以使用 PyPI 从 pip 安装软件包 <Table
columns={columns}
dataSource={context.products}
rowClassName={(record,index) => (record.current_price !== record.previous_price && "green") (record.current_price === 'Timeout' && "red")}
onChange={onChange}
pagination={{ pageSize: 100 }}
/>
，如下所示：
"""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 = ' /\\ '.join(
'((x_{i} \/ y_{i}) <=> {b})'.format(i=i,b=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 = 'y_{j}'.format(j=i + 2)
else:
e = 'FALSE'
s = '((~ ({e} <=> x_{i})) <=> {b})'.format(e=e,i=i,b=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 = 'z_{j}'.format(j=i + 1)
else:
e = 'FALSE'
s = '(({e} /\ y_{i}) <=> {b})'.format(e=e,b=to_boolean(b))
c.append(s)
conjunct_3 = ' /\\ '.join(c)
# form fourth conjunct
c = list()
for i,b in enumerate(bitvalues[3]):
# left shift by 2
if i > 1:
e = 'x_{j}'.format(j=i - 2)
else:
e = 'FALSE'
s = '(({e} \/ z_{i}) <=> {b})'.format(e=e,b=to_boolean(b))
c.append(s)
conjunct_4 = '/\\'.join(c)
# conjoin formulas to form problem description
formula = ' /\\ '.join(
'({u})'.format(u=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('{n} solutions:'.format(n=n_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)
输出还包括对问题进行编码的 TLA+ 公式：
4 solutions:
[{'x': 16673,'y': 18603,'z': 4871},{'x': 16673,'z': 4999},'z': 5895},'z': 6023}]
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。
