Quelle est la manière la plus élégante de trouver des nombres de 16 bits qui satisfont à certaines conditions ?

Question

Je dois trouver tous les triples de nombres de 16 bits ( x , y , z ) (en fait, seulement les bits qui correspondent parfaitement dans des triples différents avec des bits sur les mêmes positions), de telle sorte que

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

Une tactique directe nécessiterait environ 2 jours sur 8700K, ce qui est trop (même si j'utilise tous les PC auxquels j'ai accès (R5-3600, i3-2100, i7-8700K, R5-4500U, 3xRPi4, RPi0/W), cela prendrait trop de temps).

Si le décalage de bits n'était pas dans les équations, il serait trivial de faire cela, mais avec les décalages, il est trop difficile de faire la même chose (ou peut-être même impossible).

J'ai donc trouvé une solution assez intéressante : analyser les équations en déclarations sur les bits des nombres (quelque chose comme "3ème bit de x XOR 1er bit de y est égal à 1") et avec toutes ces déclarations écrites dans quelque chose comme le langage Prolog (ou simplement les interpréter en utilisant les tables de vérité des opérations), tous les bits non ambigus exécutés seraient trouvés. Cette solution est également assez difficile à mettre en œuvre : Je n'ai aucune idée de la manière d'écrire un tel analyseur et aucune expérience en Prolog. (*)

La question est donc la suivante : quelle serait la meilleure façon de procéder ? Et si c'est (*), comment faire ?

Edit : pour faciliter le codage, voici le schéma binaire des nombres :

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

Answer 1

Il existe quatre solutions. Dans chacune d'elles, x = 0x4121, y = 0x48ab. Il y a quatre options pour z (deux de ses bits sont libres de prendre la valeur 0 ou 1), à savoir 0x1307, 0x1387, 0x1707, 0x1787.

Cela peut être calculé en traitant les variables comme des tableaux de 16 bits et en implémentant les opérations sur les bits en termes d'opérations sur les booléens. Cela pourrait probablement être fait en Prolog, ou avec un solveur SAT ou avec des diagrammes de décisions binaires. ce site web qui utilise les BDD en interne.

Answer 2

En voici un qui utilise le logiciel SWI-Prolog's library(clpb) pour résoudre les contraintes sur les variables booléennes (merci Markus Triska !).

Traduction très simple (je n'ai jamais utilisé cette bibliothèque mais c'est assez simple) :

:- 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).

Nous trouvons plusieurs solutions en 0,007 seconde, en ajoutant les traductions en hexadécimal (travail manuel) :

?- 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

Voici une implémentation en Picat avec mon module bitwise expérimental ( http://hakank.org/picat/bitwise.pi ) en utilisant la programmation par contraintes. Cela a pris 0.007s sur ma machine. Le modèle est également ici : 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.

Le résultat :

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

Cependant, pour effectuer ce type de calcul de bits, z3 ( https://github.com/Z3Prover/z3 ) est probablement la meilleure solution, à la fois en termes de modélisation et de fonctionnalités : il gère des tailles longues arbitraires, etc.

Voici un modèle de z3 utilisant l'interface Python (également ici : 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)

Sortie :

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

Answer 5

Une solution Python utilisant les BDD et les vecteurs de bits, avec le paquetage 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 = ' /\\ '.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, i=i, 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, i=i, 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)

La sortie donne les solutions :

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}]

qui est d'accord avec les autres réponses données ici.

Le paquet omega peut être installé à partir de PyPI en utilisant pip comme suit :

pip install omega

La sortie comprend également le TLA+ qui codifie le problème :

(((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))