Extracción de bits con una sola multiplicación

Pregunta muy interesante. Estoy interviniendo con mis dos centavos, que es que, si puedes manejar problemas como este en términos de lógica de primer orden sobre la teoría de bitvector, entonces los probadores de teoremas son tu amigo, y potencialmente pueden proporcionarte respuestas muy rápidas a tus preguntas. Vamos a re-establecer el problema que se pregunta como un teorema:

" Existen algunas constantes de 64 bits 'mask' y 'multiplicand' tales que, para todos los vectores de bits de 64 bits x, en la expresión y =(x & mask) * multiplicand / multiplicando, tenemos que y.63 == x.63, y.62 == x.55, y.61 == x.47, etc."

Si esta oración es de hecho un teorema, entonces es cierto que algunos valores de las constantes 'mask' y 'multiplicand' satisfacen esta propiedad. Así que vamos a expresar esto en términos de algo que un probador de teoremas puede entender, a saber, SMT-LIB 2 entrada:

(set-logic BV)

(declare-const mask         (_ BitVec 64))
(declare-const multiplicand (_ BitVec 64))

(assert
  (forall ((x (_ BitVec 64)))
    (let ((y (bvmul (bvand mask x) multiplicand)))
      (and
        (= ((_ extract 63 63) x) ((_ extract 63 63) y))
        (= ((_ extract 55 55) x) ((_ extract 62 62) y))
        (= ((_ extract 47 47) x) ((_ extract 61 61) y))
        (= ((_ extract 39 39) x) ((_ extract 60 60) y))
        (= ((_ extract 31 31) x) ((_ extract 59 59) y))
        (= ((_ extract 23 23) x) ((_ extract 58 58) y))
        (= ((_ extract 15 15) x) ((_ extract 57 57) y))
        (= ((_ extract  7  7) x) ((_ extract 56 56) y))
      )
    )
  )
)

(check-sat)
(get-model)

Y ahora vamos a preguntar al probador de teoremas Z3 si esto es un teorema:

z3.exe /m /smt2 ExtractBitsThroughAndWithMultiplication.smt2

El resultado es:

sat
(model
  (define-fun mask () (_ BitVec 64)
    #x8080808080808080)
  (define-fun multiplicand () (_ BitVec 64)
    #x0002040810204081)
)

Bingo! Se reproduce el resultado dado en el post original en 0.06 segundos.

Mirando esto desde una perspectiva más general, podemos ver esto como una instancia de un problema de síntesis de programas de primer orden, que es un área incipiente de investigación sobre la cual se han publicado pocos artículos. Una búsqueda de "program synthesis" filetype:pdf debería ayudarte a empezar.

Cada 1-bit en el multiplicador se utiliza para copiar uno de los bits en su posición correcta:

• 1 ya está en la posición correcta, así que multiplique por 0x0000000000000001.
• 2 debe ser desplazado 7 posiciones de bits a la izquierda, por lo que se multiplica por 0x0000000000000080 (bit 7 se establece).
• 3 debe ser desplazado 14 posiciones de bits a la izquierda, por lo que se multiplica por 0x0000000000000400 (bit 14 se establece).
• y así sucesivamente hasta
• 8 debe ser desplazado 49 posiciones de bits a la izquierda, por lo que multiplicamos por 0x0002000000000000 (bit 49 está establecido).

El multiplicador es la suma de los multiplicadores para los bits individuales.

Esto solo funciona porque los bits que se recopilan no están demasiado juntos, de modo que la multiplicación de bits que no pertenecen juntos en nuestro esquema o caen más allá del bit 64 o en la parte inferior no importa.

Tenga en cuenta que los otros bits en el número original deben ser 0. Esto se puede lograr enmascarándolos con una operación Y.

(Nunca lo había visto antes. Este truco es genial!)

Ampliaré un poco la afirmación de Floris de que al extraer n bits necesita n-1 espacio entre cualquier bits no consecutivos:

Mi pensamiento inicial (veremos en un minuto cómo esto no funciona del todo) fue que podría hacerlo mejor: Si desea extraer n bits, tendrá una colisión al extraer / desplazar bits i si tiene alguien (no consecutivo con bit i) en los i-1 bits anteriores o n-i bits posteriores.

Voy a dar algunos ejemplos para ilustrar: {[45]]}

...a..b...c... Funciona (nadie en los 2 bits después de a, el bit antes y el bit después de b, y nadie está en los 2 bits antes c):

  a00b000c
+ 0b000c00
+ 00c00000
= abc.....

...a.b....c... Falla porque b está en los 2 bits después de a (y es arrastrado al lugar de otra persona cuando cambiamos a):

  a0b0000c
+ 0b0000c0
+ 00c00000
= abX.....

...a...b.c... Falla porque b está en los 2 bits que preceden a c (y es empujado al lugar de otra persona cuando nosotros nos desplazamos c):

  a000b0c0
+ 0b0c0000
+ b0c00000
= Xbc.....

...a...bc...d... Funciona porque los bits consecutivos se desplazan juntos:

  a000bc000d
+ 0bc000d000
+ 000d000000
= abcd000000

Pero tenemos un problema. Si usamos n-i en lugar de n-1 podríamos tener el siguiente escenario: ¿qué pasa si tenemos una colisión fuera de la parte que nos interesa, algo que podría enmascarar al final, pero cuya llevar bits acaban interfiriendo en la importante de la onu-enmascarado gama? (y nota: el requisito n-1 se asegura de que esto no suceda asegurándose de que los bits i-1 después de que nuestro rango no enmascarado esté claro cuando cambiamos el ith bit)

...a...b..c...d... Potencial fallo en carry-bits, c está en n-1 después de b, pero satisface n-i criterios:

  a000b00c000d
+ 0b00c000d000
+ 00c000d00000
+ 000d00000000
= abcdX.......

Entonces, ¿por qué no volvemos a ese requisito de "n-1 bits de espacio"? Porque podemos hacerlo mejor:

...a....b..c...d.. Falla la prueba "n-1 bits de espacio", pero funciona para nuestro truco de extracción de bits:

+ a0000b00c000d00
+ 0b00c000d000000
+ 00c000d00000000
+ 000d00000000000
= abcd...0X......

No se me ocurre una buena manera de caracterizar estos campos que no tienen n-1 espacio entre bits importantes, pero aún así funcionarían para nuestra operación. Sin embargo, dado que sabemos de antemano qué bits nos interesan, podemos revisar nuestro filtro para asegurarnos de que no experimentamos colisiones de bits portadores:

Compare (-1 AND mask) * shift con el resultado esperado de todos los uno, -1 << (64-n) (para 64 bits sin signo)

El cambio mágico/multiplicar para extraer nuestros bits funciona si y solo si los dos son iguales.

Además de las ya excelentes respuestas a esta pregunta muy interesante, podría ser útil saber que este truco de multiplicación bitwise ha sido conocido en la comunidad de ajedrez por computadora desde 2007, donde va bajo el nombre de BitBoards mágicos.

Muchos motores de ajedrez de computadora usan varios enteros de 64 bits (llamados bitboards) para representar los diversos conjuntos de piezas (1 bit por cuadrado ocupado). Supongamos que una pieza deslizante (torre, alfil, reina) en un cierto el cuadrado de origen puede moverse a como máximo K cuadrados si no hay piezas de bloqueo presentes. Usando bitwise-y de esos bits dispersos K con el bitboard de cuadrados ocupados da una palabra específica K-bit incrustada dentro de un entero de 64 bits.

La multiplicación mágica se puede usar para mapear estos bits K dispersos a los bits K inferiores de un entero de 64 bits. Estos bits K inferiores se pueden usar para indexar una tabla de bitboards pre-calculados que representan los cuadrados permitidos en los que se encuentra la pieza su cuadrado de origen en realidad se puede mover a (teniendo cuidado de bloquear piezas, etc.)

Un motor de ajedrez típico que usa este enfoque tiene 2 tablas (una para torres, una para alfiles, reinas usando la combinación de ambas) de 64 entradas (una por cuadrado de origen) que contienen tales resultados pre-calculados. Tanto la fuente cerrada mejor valorada (Houdini) y motor de ajedrez de código abierto(Stockfish) actualmente utilizar este enfoque para su muy alta rendimiento.

Encontrar estos multiplicadores mágicos se hace ya sea utilizando un búsqueda exhaustiva (optimizada con cortes tempranos) o con trial y erorr (por ejemplo, probar muchos enteros aleatorios de 64 bits). No se han utilizado patrones de bits durante la generación de movimientos para los cuales no se pudo encontrar ninguna constante mágica. Sin embargo, los efectos de transporte de bits son típicamente necesarios cuando los bits a asignar tienen índices (casi) adyacentes.

AFAIK, el muy general SAT-solver approachy by @ Syzygy no ha sido utilizado en ajedrez por computadora, y tampoco parece haber ninguna teoría formal con respecto a la existencia y singularidad de tales constantes mágicas.