AI 中文总结
该研究针对F₂上的矩阵乘法SAT基准，发现10个预期不可满足的Challenge-2公式实际可满足，还构造了无3型项的秩23方案，生成了21个实例的SAT证书且可快速复现。
AI 中文摘要
Heule、Kauers和Seidl提出的矩阵乘法SAT基准测试，除其他任务外，还要求解决10个已知可满足的秩23公式、为10个预期不可满足的公式提供不可满足性证明，以及在F₂上构造一个带有不含3型单项式的加项的秩23方案。我们为commit 150b2e2f版本的仓库中顶级challenge1/、challenge2/和challenge3/目录下的21个CNF公式提供了完整的满足赋值。主要发现是，全部10个顶级Challenge-2公式均可满足。直接审计显示，它们的硬编码3型配对由621个基础变量上的正单元子句施加：这些公式要求特定关联，但不禁止额外的3型关联。我们从精确的23加项方案出发，利用GL(3,2)³各向同性作用、循环迹对称性，以及变换后加项与受限槽位的完美匹配，为全部10个文件构造了见证。对于Challenge 3，我们结合锁定语义修复与F₂上的两项恒等式，得到一个3型计数为0的特殊加项。所有语义分解在全部729个Brent方程中残差均为0。附带的DIMACS模型为每个公式的全部26541个变量赋值，并满足21个实例中的全部2461316个子句。一个独立的解析器和子句评估器对生成的模型进行重新检查。一个确定性的单文件Python复现器在报告的测试主机上，从原始CNF公式中重新生成这21个证书，耗时约9秒。
英文摘要
The matrix-multiplication SAT benchmark of Heule, Kauers, and Seidl asks, among other tasks, for solutions of ten known-satisfiable rank-23 formulas, proofs of unsatisfiability for ten formulas expected to be unsatisfiable, and a rank-23 scheme over $\mathbb{F}_2$ having a summand with no type-3 monomial. We give complete satisfying assignments for the 21 CNFs in the repository's top-level challenge1/, challenge2/, and challenge3/ directories at commit 150b2e2f. The principal finding is that all ten top-level Challenge-2 formulas are satisfiable. A direct audit shows that their hardcoded type-3 pairings are imposed by positive unit clauses on the 621 base variables: the formulas require selected incidences but do not forbid additional type-3 incidences. Starting from exact 23-summand schemes, we use the $\mathrm{GL}(3,2)^3$ isotropy action, cyclic trace symmetry, and perfect matching of transformed summands to constrained slots to construct witnesses for all ten files. For Challenge 3, we combine a locked semantic repair with a two-term identity over $\mathbb{F}_2$ to obtain a distinguished summand of type-3 count zero. Every semantic decomposition has zero residual in all 729 Brent equations. The accompanying DIMACS models assign all 26,541 variables of each formula and satisfy all 2,461,316 clauses across the 21 instances. A separate parser and clause evaluator rechecks the emitted models. A deterministic one-file Python reproducer regenerates the 21 certificates from the original CNFs in approximately nine seconds on the reported test host.
