{"id":"29551fd9-9898-41c6-9805-e816ae8a329a","arxiv_id":"2607.29291","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"All ten 'expected-UNSAT' Challenge-2 CNFs for rank-23 matrix multiplication over F2 are satisfiable, and a 23-summand scheme with a type-3-free summand exists.","lead":"This paper provides explicit Boolean satisfying assignments for all 21 top-level matrix-multiplication challenge formulas from the Heule–Kauers–Seidl repository, including the ten that were expected to be unsatisfiable. Every assigned model is checked against every clause, so the claims are machine-verifiable rather than heuristic.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Central claim rests on the author's own clause evaluator; a self-consistent parser bug or CNF-pinning error would invalidate all certificates. Independent verification of the 21 models against commit-150b2e2f is required.","rationale":"The reader's weakest assumption correctly identifies the certificate pipeline as the least secure element. My reading of the paper confirms that all theorems reduce to the empirical claim in Proposition 3.1: the author's checker accepted all files. This is not a formal proof, and no independent verifier is supplied. The paper's own reproducible artifact is a single script that both generates and checks the certificates, so a bug in that script could invalidate every conclusion without being caught internally. The check I propose is cheap and definitive: use a widely accepted third-party DIMACS model checker on the distributed .model files against the pinned CNF commit. If it passes, the central claim is confirmed; if it fails, the theorems collapse. Given that the paper's value hinges entirely on these certificates, and the certificates have not yet been independently verified, the appropriate verdict is conditional acceptance rather than unconditional acceptance.","tokens_in":10948,"tokens_out":10235,"duration_ms":113658,"concrete_test":"Using the exact upstream commit 150b2e2f519fa9896ad6dbb5103d886aa009f872, run a third-party DIMACS model checker (e.g., a standalone parser strictly following the DIMACS spec, or the model-validation utility in python-sat) on each of the 21 supplied .model files. Verify that per-file SHA-256 digests match Appendix C. If any of the 2,461,316 clauses evaluates false, Proposition 3.1, Theorem 5.3, and Theorem 6.1 fail. If all pass, the parser concern is resolved.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Proposition 3.1 is the linchpin: its proof is effectively 'the checker accepts all files.' The paper does not supply a formally verified checker or a third-party re-run. A bug in clause termination handling (e.g., accepting a clause missing its terminal 0), in header count parsing, in variable ordering, or in pinning to a different commit would make all 21 models appear satisfying when they are not. Since the two-pass evaluation is written by the same author, both passes could share a subtle assumption about DIMACS format. The reproducer in Section 7.2 both generates and checks the certificates, so it is self-certified; no independent artifact validates the central claim. This is a verification gap, not a mathematical inconsistency, but it is load-bearing: every theorem in the paper depends on the certificate criterion being sound.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":11177,"tokens_out":7203,"duration_ms":81045,"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":[{"comment":"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.","section":"§3, Proposition 3.1; §7.2"},{"comment":"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.","section":"§5.3, Theorem 5.3; Appendix B"}],"minor_comments":[{"comment":"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.","section":"§3"},{"comment":"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.","section":"§5.1"},{"comment":"The notation P^{-T} is nonstandard; please define it as (P^{-1})^T or equivalently (P^T)^{-1}.","section":"§5.2, Eq. (7)"},{"comment":"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.","section":"§7.2"},{"comment":"The '69 aligned factor flips' is clear only after counting 23 summands × 3 factor types. A one-line explanation would help the reader.","section":"§4, Algorithm 1"},{"comment":"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.","section":"§Acknowledgments"},{"comment":"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.","section":"§8.1"}],"recommendation":"major_revision","confidential_remarks":"The central mathematical constructions (isotropy action, perfect matching, two-term identity) appear sound, and the certificate artifacts are a strength. My recommendation is major_revision rather than accept because the load-bearing verification step (Proposition 3.1) is only checked by the authors' own evaluator, and I was not able to rerun the artifact. This is a standard reproducibility concern for computational SAT papers; it is fixable by adding an independent, auditable checker or a third-party verification transcript. I would not reject: the methods and claims are plausible and the artifact is unusually complete."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing you need to know: the headline is real and interesting. Palladinos gives complete satisfying assignments for all ten Challenge-2 CNFs from the Heule–Kauers–Seidl benchmark, the ones marked expected-UNSAT. That is a genuine correction, not a trick: the paper audits the encodings and shows the hardcoded type-3 pairings are positive units, not exact cores, so additional type-3 incidences are allowed and even necessary. That explanation is the most valuable part of the paper. The GL(3,2)^3 isotropy action plus perfect matching construction is a neat way to get the witnesses, and the two-term identity for Challenge 3 is clean. The paper is also careful about scope: it settles the exact CNFs at a fixed commit, not the rank-22 question or exact-core variants.\n\nWhere it is soft: the entire result depends on Proposition 3.1, whose proof is effectively 'the checker accepted all files.' The checker and the reproducer are written by the same author, and the model files are self-certified in the sense that the reproducer both generates and verifies them. If there is a parser bug, a variable-ordering mistake, or a wrong commit pin, all 21 certificates could be bogus. That is a real verification gap, and it is load-bearing. It is not a mathematical inconsistency; the semantic constructions are specified precisely enough that a third party could re-run the one-file reproducer or write a trivial clause evaluator for the .model files. But nobody independent has done that yet.\n\nMinor quibbles: the paper does not provide a formally verified checker or a DRAT proof, though the .model files are simple enough that a basic script can check them. The runtime measurements are fine as reproducibility data, not a benchmark. The self-citation to the artifact repo is appropriate given that it ships code and hashes.\n\nMy take: this deserves a serious referee. The central claim is checkable, the math is small but correct, and the benchmark-design discussion is useful. I would send it to peer review with the expectation that reviewers run or inspect the artifact, and I would ask the authors to record an independent run. For my own work, I would cite it as the definitive answer for these ten CNFs once I have re-run the checker myself.","headline":"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.","tokens_in":11591,"tokens_out":2789,"would_cite":true,"duration_ms":31469,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["15A69"],"pacs":[],"model":"deepseek-v4-flash","headline":"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","keywords":["matrix multiplication","tensor rank","Boolean Brent equations","SAT certificates","type-3 monomials","GL(3,2) isotropy","cyclic trace symmetry","semantic local search"],"falsifier":"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.","tokens_in":10874,"feed_emoji":"🧮","tokens_out":4609,"duration_ms":42564,"temperature":0.7,"pith_summary":"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.","feed_headline":"All ten 'unsatisfiable' matrix-multiplication formulas are satisfiable","feed_subtitle":"Complete assignments satisfy all 2,461,316 clauses; the formulas only require type-3 incidences, not exact cores.","key_machinery":"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.","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["All ten 'expected-UNSAT' matrix formulas actually SAT","Type-3 units only require, so ten 'unsat' instances are all SAT","All ten 'impossible' matrix challenges solved: they're actually SAT","Ten 'expected-UNSAT' formulas all have satisfying assignments"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["All ten 'expected-UNSAT' matrix formulas actually SAT","Type-3 units only require, so ten 'unsat' instances are all SAT","All ten 'impossible' matrix challenges solved: they're actually SAT","Ten 'expected-UNSAT' formulas all have satisfying assignments"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001489,"raw_usage":{"total_tokens":5884,"prompt_tokens":883,"completion_tokens":5001,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":627,"completion_tokens_details":{"reasoning_tokens":4923}},"tokens_in":627,"tokens_out":5001,"duration_ms":36759,"temperature":1.0,"reasoning_tokens":4923,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T09:49:56.187667+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}