非常有趣的问题。我只是说说我的观点，如果你能在位向量理论的基础上用一阶逻辑来表述这样的问题，那么定理证明者就是你的朋友，并且可能会为你的问题提供非常快速的答案。让我们把这个问题重新表述为一个定理:

“存在一些64位常数‘mask’和‘multiplicand’，这样，对于所有64位位向量x，在表达式y = (x & mask) * multiplicand中，我们有y.63 == x.63, y.62 == x.55, y.61 == x.47等。”

如果这句话实际上是一个定理，那么常数“mask”和“multiplicand”的某些值确实满足这个性质。所以让我们用定理证明者能够理解的东西来表达它，即SMT-LIB 2输入:

(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秒内复制了原始帖子中给出的结果。

从更一般的角度来看，我们可以把它看作是一阶程序综合问题的一个实例，这是一个新兴的研究领域，很少有论文发表。搜索“程序合成”文件类型:pdf就可以开始了。

非常有趣的问题。我只是说说我的观点，如果你能在位向量理论的基础上用一阶逻辑来表述这样的问题，那么定理证明者就是你的朋友，并且可能会为你的问题提供非常快速的答案。让我们把这个问题重新表述为一个定理:

“存在一些64位常数‘mask’和‘multiplicand’，这样，对于所有64位位向量x，在表达式y = (x & mask) * multiplicand中，我们有y.63 == x.63, y.62 == x.55, y.61 == x.47等。”

如果这句话实际上是一个定理，那么常数“mask”和“multiplicand”的某些值确实满足这个性质。所以让我们用定理证明者能够理解的东西来表达它，即SMT-LIB 2输入:

(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秒内复制了原始帖子中给出的结果。

从更一般的角度来看，我们可以把它看作是一阶程序综合问题的一个实例，这是一个新兴的研究领域，很少有论文发表。搜索“程序合成”文件类型:pdf就可以开始了。

非常有趣的问题，聪明的技巧。

让我们看一个处理单个字节的简单示例。为了简单起见，使用无符号8位。假设你的数字是xxaxxbxx，你想要ab000000。

解决方案包括两个步骤:位掩码，然后是乘法。位掩码是一个简单的AND操作，将无意义的位转换为零。在上面的例子中，你的掩码是00100100，结果是00a00b00。

现在最难的部分是:把它变成ab.......

乘法是一堆移位加运算。关键是允许溢出“移走”我们不需要的位，并将我们想要的位放在正确的位置。

乘以4(00000100)会将所有元素向左移动2，得到a00b0000。为了让b上移，我们需要乘以1(让a保持在正确的位置)+ 4(让b上移)。这个和是5，加上前面的4，我们得到一个神奇的数字20，或00010100。掩模后原为00a00b00;乘法得到:

000000a00b000000
00000000a00b0000 +
----------------
000000a0ab0b0000
xxxxxxxxab......

通过这种方法，您可以扩展到更大的数字和更多的位。

你问的其中一个问题是"这能用任意数量的比特来完成吗?"我认为答案是“不”，除非你允许多次屏蔽操作，或者多次乘法。问题是“碰撞”的问题——例如，上面问题中的“杂散b”。想象一下，我们需要对xaxxbxxcx这样的数做这个运算。按照前面的方法，您可能认为我们需要{x 2, x {1 + 4 + 16}} = x 42(哦-所有问题的答案!)结果:

00000000a00b00c00
000000a00b00c0000
0000a00b00c000000
-----------------
0000a0ababcbc0c00
xxxxxxxxabc......

正如你所看到的，它仍然有效，但“只是刚刚”。这里的关键是在我们想要的比特之间有“足够的空间”，我们可以把所有东西都挤起来。我不能在c后面加第四个位d，因为我得到的实例是c+d，位可能会。

所以在没有正式的证明的情况下，我会这样回答你问题中更有趣的部分:“不，这对任何数量的比特都不适用。要提取N位，你需要在你想提取的位之间有(N-1)个空格，或者有额外的掩码乘法步骤。”

我能想到的“比特之间必须有(N-1)个零”规则的唯一例外是:如果你想提取原始数据中彼此相邻的两个比特，并且你想让它们保持相同的顺序，那么你仍然可以这样做。为了(N-1)规则的目的，它们被算作两位。

There is another insight - inspired by the answer of @Ternary below (see my comment there). For each interesting bit, you only need as many zeros to the right of it as you need space for bits that need to go there. But also, it needs as many bits to the left as it has result-bits to the left. So if a bit b ends up in position m of n, then it needs to have m-1 zeros to its left, and n-m zeros to its right. Especially when the bits are not in the same order in the original number as they will be after the re-ordering, this is an important improvement to the original criteria. This means, for example, that a 16 bit word

a...e.b...d..c..

可以转换成

abcde...........

尽管e和b之间只有一个空格，d和c之间只有两个空格，其他之间只有三个空格。N-1怎么了??在这种情况下，一个…E变成了“一个方块”——它们被乘以1，最终到达正确的位置，所以“我们免费得到了E”。对于b和d也是如此(b向右需要3个空格，d向左也需要3个空格)。所以当我们计算这个神奇的数字时，我们发现有重复的地方:

a: << 0  ( x 1    )
b: << 5  ( x 32   )
c: << 11 ( x 2048 )
d: << 5  ( x 32   )  !! duplicate
e: << 0  ( x 1    )  !! duplicate

显然，如果你想让这些数字以不同的顺序排列，你就必须把它们间隔得更远。我们可以重新表述(N-1)规则:“如果比特之间至少有(N-1)个空格，它总是有效的;或者，如果最终结果中比特的顺序是已知的，那么如果比特b最终位于第m (n)位，那么它的左边需要有m-1个零，右边需要有n-m个零。”

@Ternary指出，这个规则并不完全有效，因为可以从位中添加“刚好在目标区域的右侧”——也就是说，当我们要查找的位都是1时。继续上面的例子，在一个16位的字中有5个紧密排列的位:如果我们从

a...e.b...d..c..

为简单起见，我将位位置命名为ABCDEFGHIJKLMNOP

我们要做的计算是

ABCDEFGHIJKLMNOP

a000e0b000d00c00
0b000d00c0000000
000d00c000000000
00c0000000000000 +
----------------
abcded(b+c)0c0d00c00

到目前为止，我们认为任何低于abcde(位置abcde)的内容都无关紧要，但事实上，正如@Ternary指出的那样，如果b=1, c=1, d=1，那么位置G的(b+c)将导致位进位到位置F，这意味着位置F的(d+1)将位进位到E -，我们的结果被破坏了。注意，最不重要的位(本例中为c)右侧的空格无关紧要，因为乘法运算将导致从最不重要的位以外填充零。

所以我们需要修改(m-1)/(n-m)规则。如果有一个以上的位在右边有恰好(n-m)个未使用的位(不包括模式中的最后一位——上面的例子是“c”)，那么我们需要加强规则——我们必须迭代地这样做!

我们不仅要看满足(n-m)标准的比特数，还要看(n-m+1)的比特数，等等。我们称它们的数字为Q0(正好是n-m到下一位)，Q1 (n-m+1)，直到Q(N-1) (N-1)。然后我们冒carry if的风险

Q0 > 1
Q0 == 1 && Q1 >= 2
Q0 == 0 && Q1 >= 4
Q0 == 1 && Q1 > 1 && Q2 >=2
... 

如果你看这个，你会发现如果你写一个简单的数学表达式

W = N * Q0 + (N - 1) * Q1 + ... + Q(N-1)

，结果为W > 2 * N，则需要将RHS准则增加一位至(N -m+1)。此时，只要W < 4，操作就是安全的;如果这不起作用，就再增加一个标准，等等。

我认为遵循上面的方法会让你找到答案。

乘数中的每一个1位都用于将其中一个位复制到正确的位置:

1已经在正确的位置，所以乘以0x0000000000000001。 2必须向左移动7位，因此我们乘以0x0000000000000080(设置了第7位)。 3必须向左移动14位，因此我们乘以0x0000000000000400(设置了第14位)。 以此类推，直到 8必须向左移动49位，因此我们乘以0x0002000000000000(第49位已设置)。

乘数是每个比特乘数的和。

这只是因为要收集的位不太接近，所以在我们的方案中不属于一起的位的乘法要么超过64位，要么在较低的“不关心”部分。

注意，原始数字中的其他位必须为0。这可以通过使用AND操作屏蔽它们来实现。

除了这个非常有趣的问题的优秀答案之外，知道这个位乘法技巧自2007年以来就在计算机国际象棋社区中为人所知，在那里它被称为魔术位板可能是有用的。

许多计算机象棋引擎使用几个64位整数(称为位板)来表示各种棋子集(每个被占用的方格1位)。假设一个在原点方格上滑动的棋子(车、bishop、q)在没有阻挡棋子的情况下最多可以移动到K个方格。按位使用这些分散的K位和已占用方块的位板给出一个嵌入在64位整数中的特定K位字。

神奇的乘法可以用来将这些分散的K位映射到64位整数的低K位。然后，这些低K位可以用来索引一个预先计算的位板表，该位板表示原始方块上的方块实际可以移动到的方块(照顾阻塞的方块等)。

使用这种方法的典型象棋引擎有2个包含这种预先计算结果的64个条目的表(一个用于白车，一个用于主教，皇后使用两者的组合)。最高评级的闭源(Houdini)和开源象棋引擎(Stockfish)目前都使用这种方法，因为它具有非常高的性能。

找到这些神奇的乘数可以使用穷尽搜索(通过早期截断进行优化)或反复试验(例如尝试大量随机的64位整数)。在移动生成过程中没有使用任何位模式，因此无法找到任何神奇常数。然而，当要映射的位有(几乎)相邻的索引时，按位进位效果通常是必要的。

AFAIK， @Syzygy的非常通用的sat求解方法还没有在计算机象棋中使用过，而且似乎也没有任何关于这种神奇常数的存在性和唯一性的正式理论。

(我以前从未见过它。这个技巧太棒了!)

我将扩展Floris的断言，当提取n位时，任何不连续的位之间都需要n-1个空间:

我最初的想法(我们将在一分钟内看到这是如何不工作的)是你可以做得更好:如果你想提取n位，当提取/移动位i时，如果你在前面的i-1位或后面的n-i位中有任何人(与位i不连续)，你会发生碰撞。

我举几个例子来说明:

c . . b……工作(没有人在a之后的2位，b之前和之后的位，没有人在c之前的2位):

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

c a.b……失败是因为b在a后面的2位(当我们移动a时，b被拉到其他人的位置上):

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

公元前…一个……失败是因为b在c之前的2位(当我们移动c时，b被推到其他人的位置上):

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

d公元前…………有效是因为连续的位移位在一起:

  a000bc000d
+ 0bc000d000
+ 000d000000
= abcd000000

但我们有个问题。如果我们使用n-i而不是n-1，我们可能会有下面的场景:如果我们在我们关心的部分之外有碰撞，我们会在最后屏蔽掉，但它的进位最终会干扰重要的未屏蔽范围?(注意:n-1要求确保这不会发生，当我们移动第i位时，确保我们的unmasking范围后的i-1位是清楚的)

……b . . c d…携带位的潜在失效，c在b之后的n-1，但满足n-i条件:

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

那么我们为什么不回到“n-1位空间”的要求呢? 因为我们可以做得更好:

……b . . c d . .未能通过“n-1位空间”测试，但适用于我们的位提取技巧:

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

我无法想出一个好方法来描述这些重要位之间没有n-1空格的字段，但仍然适用于我们的操作。然而，由于我们提前知道我们感兴趣的比特，我们可以检查我们的过滤器，以确保我们没有遇到进位冲突:

比较(-1 AND掩码)* shift与预期的all-one结果，-1 << (64-n)(对于64位无符号)

当且仅当两者相等时，才能使用神奇的移位/相乘来提取我们的位。