Извлечение битов с помощью одного умножения

действительно очень интересный вопрос. Я вмешиваюсь в свои два цента, а именно: если вы можете сформулировать такие проблемы с точки зрения логики первого порядка над теорией битвекторов, то доказатели теорем-ваш друг и потенциально могут предоставить вам очень быстрые ответы на ваши вопросы. Давайте переформулируем задачу, задаваемую в виде теоремы:

"существуют некоторые 64-битные константы 'mask' и 'multiplicand' такие, что для всех 64-битных битвекторов x, в выражение y = (x & mask) * multiplicand, мы имеем, что y.63 == x.63, y.62 == x.55, y.61 == x.47 и т. д."

если это предложение на самом деле теорема, то верно, что некоторые значения констант "Маска" и "мультипликация" удовлетворяют этому свойству. Итак, давайте сформулируем это в терминах того, что может понять доказатель теоремы, а именно SMT-LIB 2 input:

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

а теперь давайте спросим у доказателя теоремы Z3, является ли это теоремой:

z3.exe /m /smt2 ExtractBitsThroughAndWithMultiplication.smt2

результат это:

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

Бинго! Он воспроизводит результат, указанный в исходном сообщении, за 0,06 секунды.

"program synthesis" filetype:pdf вы должны начать.

каждый 1-бит в множителе используется для копирования одного из битов в его правильное положение:

• 1 уже находится в правильном положении, поэтому умножьте на 0x0000000000000001.
• 2 должны быть сдвинуты 7 разрядных позиций влево, поэтому мы умножаем на 0x0000000000000080 (установлен бит 7).
• 3 должны быть сдвинуты 14 разрядных позиций влево, поэтому мы умножаем на 0x0000000000000400 (установлен бит 14).
• и так далее до
• 8 необходимо сдвинуть 49 разрядных позиций влево, поэтому умножим на 0x0002000000000000 (49 бит установлен).

множитель-это сумма множителей для отдельных битов.

это работает только потому, что биты, которые нужно собрать, не слишком близки друг к другу, так что умножение битов, которые не принадлежат друг другу в нашей схеме, либо выходят за пределы 64-битной, либо в нижней части безразличия.

обратите внимание, что другие биты в исходном номере должны быть 0. Это может быть достигнуто путем маскировки их с помощью операции AND.

(я никогда не видел его раньше. Это отличный трюк!)

я немного расширю утверждение Флориса о том, что при извлечении n бит вам нужно n-1 пробел между любыми не последовательными битами:

моя первоначальная мысль (мы увидим через минуту, как это не совсем работает) заключалась в том, что вы могли бы сделать лучше: если вы хотите извлечь n бит, вы будете иметь столкновение при извлечении / сдвиге бит i если у вас есть кто-нибудь (не подряд с битом i) в i-1 биты предшествующие или n-i биты последующее.

я приведу несколько примеров для иллюстрации:

...a..b...c... работает (никто в 2 битах после a, немного до и немного после b, и никто не находится в 2 битах до c):

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

...a.b....c... терпит неудачу, потому что b находится в 2 битах после a (и втягивается в чужое место, когда мы сдвигаемся a):

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

...a...b.c... Терпит неудачу, потому что b находится в 2 битах, предшествующих c (и получает толкнул на чужое место, когда мы сдвигаем c):

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

...a...bc...d... работает, потому что последовательные биты сдвигаются:

  a000bc000d
+ 0bc000d000
+ 000d000000
= abcd000000

но у нас есть проблема. если мы используем тег n-i вместо n-1 у нас может быть следующий сценарий: что, если у нас есть столкновение за пределами той части, о которой мы заботимся, что-то, что мы замаскируем в конце, но чьи биты переноса заканчиваются до вмешательства в важный немаскированный диапазон? (и примечание:n-1 требование гарантирует, что этого не произойдет, убедившись, что i-1 биты после нашего диапазона без маски ясны, когда мы сдвигаемiой)

...a...b..c...d... потенциальный отказ на перенос битов, c находится в n-1 после b, но отвечает n-i критерии:

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

так почему бы нам просто не вернуться к этому"n-1 бит пространства" требование? потому что мы можем сделать лучше:

...a....b..c...d..не"n-1 биты пространства " тест, но работает для нашего бит-извлечения трюк:

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

я не могу придумать хороший способ, чтобы охарактеризовать эти поля не есть n-1 пространство между важными битами, но все равно будет работать для нашей операции. Однако, так как мы знаем заранее биты, которые нас интересуют, мы можем проверить наш фильтр, чтобы убедиться, что мы не опыт переноса битных столкновений:

сравнить (-1 AND mask) * shift против ожидаемого результата all-ones,-1 << (64-n) (для 64-разрядной версии без знака)

магический сдвиг / умножение для извлечения наших битов работает тогда и только тогда, когда они равны.

в дополнение к уже отличным ответам на этот очень интересный вопрос, было бы полезно знать, что этот трюк побитового умножения был известен в компьютерном шахматном сообществе с 2007 года, где он идет под названием Магия BitBoards.

многие компьютерные шахматные движки используют несколько 64-разрядных целых чисел (называемых битбордами) для представления различных наборов фигур (1 бит на занятый квадрат). Предположим, что скользящая фигура (ладья, слон, Королева) на определенном исходном квадрате может двигаться не более K квадраты, если никаких блокирующих частей не было. Используя побитовое-и из тех разбросанных K биты с bitboard занимаемых квадратов дает конкретные K-битовое слово, встроенное в 64-разрядное целое число.

магическое умножение может быть использовано для отображения этих рассеянных K бит до нижнего K биты 64-разрядного целого числа. Эти ниже K биты могут быть использованы для индексирования таблицы предварительно вычисленных битовых панелей, которые представляет разрешенные квадраты, на которые может фактически переместиться фигура на исходном квадрате (заботясь о блокировке фигур и т. д.)

типичный шахматный движок, использующий этот подход, имеет 2 таблицы (одну для ладей, одну для слонов, ферзей, использующих комбинацию обоих) из 64 записей (по одной на исходный Квадрат), которые содержат такие предварительно вычисленные результаты. Оба самых высоких номинальных закрытых источника (Гудини) и шахматный движок с открытым исходным кодом (Stockfish) в настоящее время используют этот подход для очень высокой производительности.

поиск этих магических множителей выполняется либо с помощью исчерпывающий поиск (оптимизировано с ранними отсечениями) или с проб и ошибок (например, пробует много случайных 64-разрядных целых чисел). Не было никаких битовых шаблонов, используемых во время генерации движения, для которых не было найдено никакой магической константы. Тем не менее, побитовый перенос эффекты обычно необходимы, когда подлежащие отображению биты имеют (почти) смежные индексы.

AFAIK, очень общий подход SAT-решателя @Syzygy не использовался в компьютерных шахматах, и, похоже, нет никакой формальной теории относительно существования и единственности таких магических констант.