What is the most elegant way to find 16-bit numbers which satisfy some conditions?

Question

I need to find all triples of 16-bit numbers (x, y, z) (well, actually only bits which perfectly match up in different triples with bits on same positions), such that

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

Straight ahead tactics would require about 2 days on 8700K, which is too much (even if I'll use all PCs I have access (R5-3600, i3-2100, i7-8700K, R5-4500U, 3xRPi4, RPi0/W) it would take too much time).

If bit shift wasn't in equations then it would be trivial to do that, but with shifts it's too hard to do the same thing (or maybe even impossible).

So I came up to pretty interesting solution: parse equations into statements about bits of numbers (something like "3rd bit of x XOR 1st bit of y is equal 1") and with all these statements written in something like Prolog language (or just interpret them using truth tables of operations) executed all unambiguous bits would be found. This solution is pretty hard too: I have no idea how to write such parser and no experience in Prolog. (*)

So the question is: What would be the best way to do this? And if it's (*) then how to do that?

Edit: for easier coding here the binary pattern of the numbers:

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

Cranial

If you can transform it into a conjunctive normal form propositional sentence over the 3 x 16 booleans, then you can feed it to a SAT solver. – Abrego

Answer 1

There are four solutions. In all of them, x = 0x4121, y = 0x48ab. There are four options for z (two of its bits are free to be 0 or 1), namely 0x1307, 0x1387, 0x1707, 0x1787.

This can be calculated by treating the variables are arrays of 16 bits and implementing the bitwise operations on them in terms of operations on booleans. That could probably be done in Prolog, or it could be done with a SAT solver or with binary decisions diagrams, I used this website which uses BDDs internally.

Wynnie

"Fast service, solution guaranteed" – Abrego

Answer 2

Here is one using SWI-Prolog's library(clpb) to solve constraints over boolean variables (thanks Markus Triska!).

Very simple translation (I have never used this library but it's rather straightforward):

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

We find several solutions in 0.007 seconds, with the translations to hexadecimal (manual work) added:

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

Abrego

Answer 3

Here is an implementation in Picat with my experimental bitwise module (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.

The output:

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]

Annieannihilate

Answer 4

However, for doing these kind of bit calculation, z3 (https://github.com/Z3Prover/z3 ) is probably the way to go, both in terms of modelling and features: it handle arbitrary long sizes, etc.

Here's a z3 model using the Python interface (also here: 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)

Output:

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

Annieannihilate

Answer 5

A Python solution using BDDs and bitvectors, with the package 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)

The output gives the 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}]

which agree with the other answers posted here.

The package omega can be installed from PyPI using pip as follows:

pip install omega

The output also includes the TLA+ formula that encodes the problem:

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

Hoopen