问题
半群计数枚举（23 号的 «实验侧»）：阶 10 的枚举用了数年计算（Distler–Kelsey 线的 GAP Semigroups 库工程， «等价类剪枝» 的代数算法）；阶 11、12 的枚举是 «计算代数的下一座山»——需要新的对称性利用或 SAT/约束求解技术。 «枚举» 的三重困难：①乘法表空间 2 的 «n² log n» 位；②结合律约束的 «非局部» 性（ «三重积» 的检查是 O(n³) 每表）；③同构类的 «剪枝» 需要 «规范形» 算法（ «图同构» 型困难）。
主要概念
等价类剪枝与规范形
枚举的 «代数剪枝»：利用 «半群的 «反同构»»（对合）、 «极小理想结构»（ «主因子分解» 的 «骨盆» 分类）与 «幂等结构» 缩小搜索空间。 «规范形»（每个同构类取一个代表）的算法： «最小乘法表» 的字典序规范（ «图规范形» 的 «带约束» 版）—— «规范形算法» 的效率决定枚举的 «深度»。
SAT/约束求解路线
«结合律» 是 «三元约束»——可编码为 SAT/CP（ «乘法表» 的 «格点» 变量、 «三重积等式» 为子句）；«SAT 求解器» 的 «CDCL» 技术对 «对称破缺»（同构剪枝）有 «现成» 工具（ «静态对称破缺» 的 lex-leader 约束）。 «半群枚举» 的 SAT 化是 «可行» 的候选路线， «规模»（阶 11 的变量数 ~ 121 log 11 ≈ 420 个 «位»、子句数 ~ n³·n = 11⁴ ≈ 1.5 万）在 SAT 能力的 «舒适区»—— «工程壮举» 的下一阶有望。
主要命题与证明
命题 1（结合律的 SAT 编码；完整证明） 半群乘法表（n² 个 «格点» 变量，每变量 log₂ n 位）的结合律可编码为 O(n⁴) 个 «位级» 子句的 SAT 实例，且解与 «结合乘法表» 一一对应。
证明 变量 T(a,b) 的 «位» T(a,b)k（k ≤ ⌈log₂ n⌉）编码 «a·b 的值»；结合律 «(ab)c = a(bc)» 对一切三元组：T(T(a,b),c) = T(a,T(b,c))—— «嵌套变量» 的 «位等式» 编码为 «标准 SAT»（ «变量等于变量的位» 子句：(xk ↔ yk) 的 CNF： (¬xk ∨ yk)∧(xk ∨ ¬yk)）。 «嵌套» 的 «T(T(a,b),c)» 依赖 «中间值»：引入 «辅助选择» 变量（ «若 ab = d 则 T(d,c) = …» 的 «大开关» 编码，O(n) 个 «条件» 每三元组），总子句 O(n⁴)。□
命题 2（枚举树与同构剪枝的完备性；陈述） GAP Semigroups 库的枚举算法（ «主理想扩展» 的枚举树）是完备的（每个同构类恰出现一次的 «规范父» 结构），其 «深度» 由 «极小理想分解» 的 «骨盆» 结构控制； «阶 10 的完成» 是该算法的当前极限（数年 CPU 时间）；阶 11 的 «剪枝率» 若无新对称性，预计算力需求增长 ≥ 10² 倍。
现状说明 «新对称性» 的候选： «反同构对» 的 «双计数»、 «幂等 «子格»» 的 «格同构» 剪枝、 «极大子群» 的 «群枚举» 复用（Pyber 型 «群稀疏»）、以及 «SAT 对称破缺» 的自动 lex-leader。 «技术路线» 的选择（代数剪枝 vs SAT vs 混合）是工程决策与 «理论瓶颈»（规范形算法的复杂度）的联合问题。□
命题 3（群的对照与 «数据-理论桥»；陈述） 群侧的枚举（阶 ≤ 2000 的全部群，GAP 小群库）已 «完成»（1990 年代工程）；半群侧的 «阶 11、12» 完成后， «23 号渐近» 的 «小 n 数据» 将延伸两位数—— «渐近公式的 «小 n 偏差»» 的定量分析（ «对数渐近的 «达域»»）是枚举的 «理论红利»。
现状说明 «小群库» 的工程史（Besche–Eick–O'Brien）展示 «枚举完成后» 的 «理论反哺»（ «绝大多数群是 2-群» 的计数现象等）；半群枚举的 «下一阶» 若完成， «两层结构主导»（23 号 KRS）的 «达域» 分析有望成为第一个 «反哺» 结果。□
进展与文献
Distler–Kelsey 的 GAP Semigroups 库系列（2009–2018）；Besche–Eick–O'Brien 的小群库工程；Araújo–Schneider 的半群计算综述；SAT 对称破缺的 Crawford 等技术文献。开放核心：阶 11、12 的枚举完成； «规范形算法» 的复杂度下界； «SAT vs 代数» 路线的比较研究。