主要观点：2025 年 1 月 Jane Street 发布一个数独谜题，要求在网格中填入数字，使每行、每列和每个 3x3 框包含 9 个不同数字，且 9 行形成的 9 位数 GCD 最大，部分格子已填好，答案是完成网格后的中间行数字。
关键信息：

• 用 SMT 优化问题和 Z3 求解未成功。
• 观察得出 GCD x≤111111111，通过枚举 x 的值，用回溯搜索和各种优化方法（如使用 bitset 和 SIMD 等）来寻找有效解。
• 多线程可加快速度，最后通过合理分配线程处理范围和使用 SIMD 优化后的代码在 360ms 内完成，且硬编码答案最快为 0ms。
  重要细节：
• is_good函数通过位运算判断数字是否有 9 个不同数字，用 SIMD 优化后速度大幅提升。
• is_good_many函数用于同时检查多个数字是否有 9 个不同数字，通过特殊的浮点位操作实现。
• 代码中通过各种循环、位运算和 SIMD 操作来处理数独谜题的约束条件和寻找解。不同优化方法的时间和速度提升情况如下：Z3 几小时未完成，用 HashSet 暴力搜索需 589s，用 bitset 暴力搜索需 15.1s，用 bitset 和多线程需 2.2s，用 SIMD 和多线程需 1.5s，用 SIMD、chunking 和多线程需 1.3s，用 SIMD、chunking 和 uncontended 多线程需 360ms，硬编码答案最快为 0ms。