Pith. sign in

REVIEW 2 major objections 7 minor 10 references

This paper proves that all ten Challenge-2 CNFs from the matrix-multiplication SAT benchmark—advertised as expected-UNSAT—are actually satisfiable, because the formulas' type-3 constraints are positive incidences that do not forbid extra ty

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-03 09:49 UTC pith:SZXZYZ3L

load-bearing objection All ten 'expected-UNSAT' matrix-multiplication CNFs turn out to be satisfiable; the result is genuinely interesting and the certificate pipeline is convincing, but an independent re-run is needed before full confidence. the 2 major comments →

arxiv 2607.29291 v1 pith:SZXZYZ3L submitted 2026-07-31 cs.SC cs.LO

SAT Certificates for the Matrix-Multiplication Challenges over F2: All Ten `Expected-UNSAT` Instances Are Satisfiable, and a Type-3-Free Rank-23 Scheme

Nick Palladinos This is my paper
classification cs.SC cs.LO MSC 15A69
keywords matrix multiplicationtensor rankBoolean Brent equationsSAT certificatestype-3 monomialsGL(3,2) isotropycyclic trace symmetrysemantic local search
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper establishes that all ten Challenge-2 CNFs in the matrix-multiplication SAT benchmark, formulas that were expected to be unsatisfiable, actually have satisfying assignments. The reason is a mismatch between the benchmark's intended semantics and its encoding: the formulas use positive unit clauses to require certain type-3 term pairings but never forbid additional type-3 incidences. The author constructs witnesses by transporting exact 23-summand decompositions through a tensor-symmetry group and matching the transformed summands to the constrained slots. The paper also produces a rank-23 scheme over F2 whose designated summand has zero type-3 monomials, answering Challenge 3. All 21 certificates assign all variables and satisfy every clause.

Core claim

The central claim is that the ten Challenge-2 formulas, advertised as expected-UNSAT, are satisfiable as encoded. Auditing the base variables shows every direct constraint is a positive unit clause; nothing in the CNF forbids additional type-3 incidences. Starting from a known 23-summand scheme, the author applies the GL(3,2)^3 isotropy action and cyclic trace symmetry, then uses perfect matching to place transformed summands into the slots forced by the units. The resulting semantic assignments propagate to full DIMACS models that satisfy all clauses. Separately, a two-term identity over F2 lets the author modify a decomposition so that one summand contains no type-3 monomial, satisfying th

What carries the argument

The central objects are the 729 Brent parity equations over F2 in 621 base variables; the GL(3,2)^3 automorphism group of the matrix-multiplication tensor (the group of triples of 3x3 invertible matrices over the two-element field, with the cyclic trace symmetry T(Z,X,Y)=tr(XYZ)); and a two-term rank-preserving identity, 92⊗89 + 438⊗24 = 92⊗65 + 490⊗24, that replaces two rank-one summands while preserving the tensor. Automorphisms generate candidate summands, perfect matching assigns them to the positively constrained slots, and unit propagation recovers the 25,920 Tseitin auxiliary variables.

Load-bearing premise

The validity of every certificate rests on the correctness of the custom parser and clause evaluator, and on the CNFs being exactly those at commit 150b2e2f; a subtle parsing or hashing bug would invalidate all satisfiability claims.

What would settle it

Take any of the 21 distributed .model files and the corresponding CNF at commit 150b2e2f and evaluate the assignment with an independently written DIMACS checker. If even one clause is falsified, the central claims collapse; the paper's own checker is currently the only verification, so independent rechecking is the decisive test.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • The ten Challenge-2 CNFs are proved satisfiable, so their advertised UNSAT status was an artifact of the encoding, not a fact about rank-23 schemes.
  • Any future 'exact-core' version of the benchmark must add negative or exact-cardinality constraints to forbid extra type-3 incidences.
  • The 21 complete assignments provide a definitive, plain-assignment resolution of the top-level Challenge-1 through Challenge-3 instances at the audited commit.
  • The type-3-free summand construction shows that the Challenge-3 constraint does not force the minimal scheme length above 23.
  • Challenge 4, the existence of a rank-22 scheme, remains open.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the original conjecture concerned the intended sparse cores, a natural test is to add negative unit clauses or exact-cardinality constraints prohibiting extra type-3 incidences and rerun; the current result suggests such tighter formulas would be genuinely harder and possibly UNSAT.
  • The symmetry-transport plus perfect-matching technique could be reused to search for rank-22 schemes by enumerating orbit representatives more efficiently than raw CNF search.
  • The two-term identity generalizes to any pair of rank-one summands sharing one factor, offering a general tool for constructing summands with prescribed local properties in other tensor decompositions.
  • Benchmark designers may want to publish a side-constraint manifest alongside CNFs, distinguishing required incidences, forbidden incidences, and parity constraints, to avoid similar encoding mismatches.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 7 minor

Summary. The paper studies the Heule–Kauers–Seidl matrix-multiplication SAT benchmark at repository commit 150b2e2f and claims that all 21 top-level CNFs in challenge1/, challenge2/, and challenge3/ are satisfiable. The main result is that the ten Challenge-2 formulas, previously expected to be unsatisfiable, are all satisfiable as encoded. The authors give a semantic local-search method on 621 base variables, use the GL(3,2)^3 isotropy action and cyclic trace symmetry to transport exact 23-summand schemes, and assign transformed summands to constrained slots via perfect matching. They also construct a rank-23 decomposition with a distinguished summand of type-3 count zero, using a locked repair step and a two-term identity over F2. Complete DIMACS assignments for all 21 instances are claimed to assign all 26,541 variables per file and satisfy all 2,461,316 clauses, with a deterministic one-file reproducer and per-instance hashes provided in the artifact repository.

Significance. If the certificate claims are correct, the paper resolves the open benchmark status of Challenge 2: the ten "expected-UNSAT" instances are in fact satisfiable. It also provides a constructive type-3-free rank-23 scheme for Challenge 3, which is a strong data point for the matrix-multiplication literature. The paper is commendably concrete: it publishes hashes for all models, a deterministic reproducer, explicit GL(3,2)^3 group elements in Table 2, and a complete 23-summand decomposition in Appendix A. The use of tensor symmetries to reduce the search to a matching problem is a genuine methodological contribution. The principal weakness is not mathematical but verification-related: the central claims rest on the correctness of the authors' own clause evaluator, which is not independently validated in this review.

major comments (2)
  1. [§3, Proposition 3.1; §7.2] The certificate criterion, and therefore Theorems 5.3 and 6.1, depends entirely on the author's two-pass checker accepting the 21 generated .model files. The proof of Proposition 3.1 is effectively 'the checker accepts all files.' Since a parser or clause-termination bug would invalidate every theorem, this is load-bearing. The manuscript should provide an independent verification path: for example, a minimal standalone checker that is short enough to audit, or hashes/transcripts produced by a widely recognized third-party SAT assignment checker. The current 'separate parser' is still written by the same author and could share a common assumption about DIMACS formatting. This is fixable within the paper's scope but needs to be addressed.
  2. [§5.3, Theorem 5.3; Appendix B] The proof of Theorem 5.3 refers to 'the stated source seed, optional cyclic rotation, GL(3,2)^3 triple, and deterministic perfect matching' but the actual source semantic assignments and matching permutations are not included in the paper; they are only generated by the reproducer. This makes the theorem's constructive claim not fully checkable from the printed text. I recommend including the source 23-summand scheme(s) from MM-23-2-2-2-2-A.cnf in an appendix, or at least the final permuted assignment for each Challenge-2 instance, so that a reader can verify zero tensor residual without trusting the artifact's search phase.
minor comments (7)
  1. [§3] Proposition 3.1 is not a proof in the usual mathematical sense. Consider relabeling it as a 'verification claim' and explicitly state the trust boundary: the result holds if the author's checker and the SHA-256-pinned CNFs are correct.
  2. [§5.1] The 'direct audit' of base-only clauses (positive units, no negative units, no non-unit base-only clauses) is stated as fact but no audit script or command is given. Adding the script or a manifest of base-only clauses would make this reproducible.
  3. [§5.2, Eq. (7)] The notation P^{-T} is nonstandard; please define it as (P^{-1})^T or equivalently (P^T)^{-1}.
  4. [§7.2] The SHA-256 digest of the reproducer is broken across lines in a confusing way. Present it as a single continuous 64-character hex string.
  5. [§4, Algorithm 1] The '69 aligned factor flips' is clear only after counting 23 summands × 3 factor types. A one-line explanation would help the reader.
  6. [§Acknowledgments] The acknowledgment to GPT-5.6 Sol is unusual and may require journal-specific disclosure. At minimum, clarify what type of assistance was used and whether the authors take full responsibility for correctness.
  7. [§8.1] The phrase 'dense orbit representatives' is slightly informal. Consider defining the density and explaining why orbits of GL(3,2)^3 tend to increase type-3 incidence beyond 27.

Circularity Check

0 steps flagged

No significant circularity: the certificates are constructive witnesses checked against the external benchmark CNFs, not predictions of fitted parameters.

full rationale

The paper's central claims are satisfiability certificates for 21 externally fixed CNF files from the matrix-challenges repository at commit 150b2e2f. Each certificate is a complete DIMACS assignment, and the paper reports that every clause of every original CNF is independently evaluated (2,461,316 clauses, zero failures). This is a direct check against an external benchmark, not a derivation from the target result. The Challenge-2 constructions start from an exact 23-summand scheme, apply the GL(3,2)^3 action (proven in Lemma 5.2 to preserve the tensor), and match transformed summands to forced unit clauses; this is model construction, and the resulting assignments are then verified clause-by-clause. The Challenge-3 construction uses a locked repair plus a rank-preserving identity (Eq. 10); the identity is algebraically correct and does not assume the conclusion. The only self-citation is the companion artifact repository, which is a pointer to the independently checkable models and code, not an unverified theorem used as evidence. The paper's main weakness is that the final clause checker is written by the same author, so a parser or pinning bug would invalidate the certificates; however, that is a verification/reproducibility risk, not circularity. No fitted parameter is relabeled as a prediction, and no load-bearing result is imported solely from the authors' prior work. The derivation chain is self-contained relative to the external benchmark inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 0 invented entities

The central claim rests on standard tensor algebra and the trustworthiness of the author's parser/checker and repository pinning. Search hyperparameters (seeds, densities, budgets) are algorithm choices, not free parameters: the emitted models are checked against the original clauses, so correctness does not require those choices to be optimal.

axioms (5)
  • standard math Brent equations (1) with target δ_i2,j1 δ_j2,k1 δ_k2,i1 formalize 3x3 matrix multiplication over F2.
    Used throughout; standard algebraic modeling of bilinear algorithms (Section 2.1).
  • domain assumption The pinned CNFs at commit 150b2e2f have the stated 26,541-variable structure, with variables 1-621 as base factors and the rest Tseitin auxiliaries.
    The audit and certificate checks depend on this structure (Sections 2.3 and 5.1); verified only by the author's parser.
  • domain assumption Repeated unit propagation from a consistent base-variable assignment completes a unique total assignment in these Tseitin encodings.
    Stated in Section 3 and used to build models; final models are checked, but the propagation claim itself is not proven in the paper.
  • standard math The GL(3,2)^3 action (7) and cyclic trace permutation preserve the target tensor.
    Proved in Lemma 5.2 using the trace identity; standard isotropy of matrix multiplication.
  • domain assumption The Challenge-3 base-level constraints (8) encode exactly 'no type-3 monomial' in the distinguished summand.
    Used in Theorem 6.1's type-3 count; relies on the repository's CNF semantics.

pith-pipeline@v1.3.0-daily-deepseek · 10709 in / 20281 out tokens · 199064 ms · 2026-08-03T09:49:56.187667+00:00 · methodology

0 comments
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2607.29291 by Nick Palladinos.

Figure 1
Figure 1. Figure 1: The common pipeline. Only the semantic construction differs among the three challenge families. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

10 extracted references · 3 canonical work pages · 1 internal anchor

  1. [1]

    Richard P. Brent. Algorithms for matrix multiplication. Technical Report CS-TR-70-157, Department of Computer Science, Stanford University, March 1970. URL https://maths-people.anu.edu.au/ brent/pub/pub002.html

    1970

  2. [2]

    A New General-Purpose Method to Multiply 3x3 Matrices Using Only 23 Multiplications

    Nicolas T. Courtois, Gregory V. Bard, and Daniel Hulme. A new general-purpose method to multiply \(3 3\) matrices using only 23 multiplications. Computing Research Repository, abs/1108.2830, 2011. https://doi.org/10.48550/arXiv.1108.2830 doi:10.48550/arXiv.1108.2830

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.1108.2830 2011

  3. [3]

    de Groote

    Hans F. de Groote. On varieties of optimal algorithms for the computation of bilinear mappings. I. The isotropy group of a bilinear mapping. Theoretical Computer Science, 7(1):1--24, 1978. https://doi.org/10.1016/0304-3975(78)90038-5 doi:10.1016/0304-3975(78)90038-5

    doi:10.1016/0304-3975(78)90038-5 1978

  4. [4]

    Marijn J. H. Heule, Manuel Kauers, and Martina Seidl. Local search for fast matrix multiplication. In Mikol\'a s Janota and In\^es Lynce, editors, Theory and Applications of Satisfiability Testing -- SAT 2019, volume 11628 of Lecture Notes in Computer Science, pages 155--163. Springer, 2019a. https://doi.org/10.1007/978-3-030-24258-9_10 doi:10.1007/978-3-...

    work page doi:10.1007/978-3-030-24258-9_10 2019

  5. [5]

    Marijn J. H. Heule, Manuel Kauers, and Martina Seidl. Matrix challenges: Challenging SAT benchmarks for matrix multiplication. GitHub repository, 2019b. URL https://github.com/marijnheule/matrix-challenges. Accessed 30 July 2026; audited revision 150b2e2f519fa9896ad6dbb5103d886aa009f872

    2026

  6. [6]

    Marijn J. H. Heule, Manuel Kauers, and Martina Seidl. New ways to multiply \(3 3\)-matrices. Journal of Symbolic Computation, 104:899--916, 2021. https://doi.org/10.1016/j.jsc.2020.10.003 doi:10.1016/j.jsc.2020.10.003

    work page doi:10.1016/j.jsc.2020.10.003 2021

  7. [7]

    Laderman

    Julian D. Laderman. A noncommutative algorithm for multiplying \(3 3\) matrices using 23 multiplications. Bulletin of the American Mathematical Society, 82(1):126--128, 1976. https://doi.org/10.1090/S0002-9904-1976-13988-2 doi:10.1090/S0002-9904-1976-13988-2

    doi:10.1090/s0002-9904-1976-13988-2 1976

  8. [8]

    A rank 23 algorithm for multiplying \(3 3\) matrices with an arithmetic complexity of 59

    Erik M rtensson, Paul Stankovski Wagner, and Joshua Stapleton. A rank 23 algorithm for multiplying \(3 3\) matrices with an arithmetic complexity of 59. arXiv preprint arXiv:2601.05272, 2026. https://doi.org/10.48550/arXiv.2601.05272 doi:10.48550/arXiv.2601.05272

    doi:10.48550/arxiv.2601.05272 2026

  9. [9]

    SAT certificates for the matrix-multiplication challenges over \( _2\): Reproducibility artifact

    Nick Palladinos. SAT certificates for the matrix-multiplication challenges over \( _2\): Reproducibility artifact. GitHub repository, 2026. URL https://github.com/palladin/sat-challenges. Accessed 31 July 2026; archived revision 41d912dcb1bcb3cde4ecfb70ffe4a4eb265b4027

    2026

  10. [10]

    Grigori S. Tseitin. On the complexity of derivation in propositional calculus. In J\"org H. Siekmann and Graham Wrightson, editors, Automation of Reasoning: Classical Papers on Computational Logic 1967--1970, pages 466--483. Springer, 1983. https://doi.org/10.1007/978-3-642-81955-1_28 doi:10.1007/978-3-642-81955-1\_28 . English translation of the 1968 original

    doi:10.1007/978-3-642-81955-1_28 1967