{"id":"bcfdeab1-6345-4331-bd8e-8211cf7acc2f","arxiv_id":"2505.01930","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A matrix-product (tensor-train-like) representation of Boolean functions, built from row-switching matrices, is proven to be a canonical normal form equivalent to quasi-reduced binary decision diagrams.","lead":"This paper proposes a new way to store Boolean functions as chains of binary matrices, inspired by quantum many-body physics. The authors show the format is a canonical normal form, equivalent to binary decision diagrams, and provide a full set of manipulation operations plus an open-source library.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The central claim depends on CLEAN converging to a unique canonical BMP; the paper asserts this with no termination, complexity, or order-independence proof, and every operation routes through CLEAN.","rationale":"The stress-test pass confirms the reader's conditional assessment. The paper's strongest claim has two parts: (i) the Shannon/compression construction of Eq. (7) is a canonical normal form for a fixed variable order, and (ii) CLEAN returns arbitrary products to that form efficiently. Part (i) rests on a reasonable uniqueness argument, although the stated form is 'up to permutations' and no deterministic row-ordering rule is given. Part (ii), which every BMP operation depends on, is asserted but not proved: Sec. IV.A provides a procedural description with no termination argument, no monotone size measure, and no complexity bound. The Appendix's SU decomposition chooses row order by first appearance in a hash table, so the cleaned output is input-order-dependent unless an additional normalization step is specified; the paper does not specify such a step. The paper's own admitted limitations, such as the lack of a killer application and open problems in bond-dimension control, are honest utility caveats rather than correctness objections. The proposed test directly decides whether the CLEAN gap is merely a missing proof or an actual algorithmic failure: instrument the shipped Julia library, run CLEAN on small non-canonical products, and check termination and order-independence. Therefore the appropriate verdict remains conditional: accept if the CLEAN convergence property is supplied and verified, otherwise the closure claim for BMP operations is unsupported.","tokens_in":23134,"tokens_out":12495,"duration_ms":137960,"concrete_test":"Use the authors' Julia library [47] on small non-canonical matrix products, e.g., the APPLY direct-product output for f = x2*x0 and g = x2*x1*x0 from Sec. V, random products of two or three canonical BMPs, and products obtained by permuting rows of canonical BMPs. Iterate LTR and RTL CLEAN sweeps until no bond dimension decreases and record the per-iteration bond dimensions. Check whether (i) sweeps terminate on all cases, (ii) the final BMP is independent of the initial row/column order for the same Boolean function, and (iii) total runtime scales polynomially with the input BMP volume. A single cycle, a non-terminating sweep, or an order-dependent fixed point would disprove the canonicalizer claim as stated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing condition is that CLEAN (Sec. IV.A, Eqs. (25)-(33)) maps an arbitrary matrix product to the canonical BMP of Eq. (7) in polynomial time. The paper states this as an assertion: 'manipulations of BMPs that can be performed efficiently lead to matrix products that can be compressed into canonical form with a polynomial number of steps' (Sec. IV.A). But Sec. III only proves uniqueness for the sequential Shannon/compression construction of Eq. (7), not for the LTR/RTL sweep applied to a general product. No termination argument or complexity bound is given, and the note that 'Reaching a canonical form requires at least one round of LTR-cleaning' (Sec. IV.A.2) is not accompanied by a proof that the sweep schedule converges. Moreover, the SU decomposition in the Appendix (Algorithm 1) assigns row labels by order of first appearance in a hash table, not by a lexicographic rule; even a fixed point of CLEAN is therefore defined only up to arbitrary row/column permutations, and no normalization to the claimed unique representative is specified. Since APPLY (Sec. IV.B), RESTRICT, JOIN, INSERT, COMPOSE, SWAP, and REORDER all call CLEAN to restore normal form, a non-terminating or order-dependent CLEAN would invalidate the central claim that BMP operations are closed on a canonical representation. The paper does honestly flag the absence of a killer application, but that is a utility caveat, not a correctness gap.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces the Binary Matrix Product (BMP) representation of Boolean functions: a product of binary row-switching matrices, built by iterated Shannon decomposition followed by compression of duplicate rows. The central claims are (i) that fully compressed BMPs form a canonical normal form for a fixed variable order, unique up to row/column permutations (Eq. (7) and Section III); (ii) that a CLEAN procedure can restore canonical form after arbitrary BMP operations in polynomial time (Section IV.A); and (iii) that BMPs are equivalent, with an explicit translation, to Binary Decision Diagrams (Section V). The paper also defines operations APPLY, RESTRICT, INSERT, JOIN, COMPOSE, SWAP, REORDER, and REVERSE ORDER, studies variable-ordering optimization via an exact A* method and sifting heuristics with experimental timings, and reports a public Julia implementation. The authors explicitly acknowledge that no killer application is demonstrated and that the practical utility depends on keeping bond dimensions polynomial.","tokens_in":23481,"tokens_out":4031,"duration_ms":42890,"significance":"If the canonicity and CLEAN-normalization claims are fully proved, the paper makes a useful contribution as a linear-algebraic reformulation of a standard data structure: BMPs are essentially layer-wise adjacency matrices of quasi-reduced BDDs, and the explicit matrix operations may lower the implementation barrier for BDD-style manipulation and connect Boolean function synthesis to the tensor-network community. The paper's strengths are its concrete Shannon-decomposition construction, the explicit BMP-to-BDD translation with worked examples, the careful treatment of APPLY by direct product versus direct sum, and the availability of an implementation. The main caveat is that the substantive novelty is representational rather than asymptotic: the paper itself notes that BDDs can be smaller than BMPs because BDDs skip levels, and that no killer application is identified. The correctness of the central claims is therefore the main gate, and the current manuscript does not yet close that gate.","major_comments":[{"comment":"The canonicity claim is stated but not proved. The text says the property follows from two elements, (a) one-variable-at-a-time iteration and (b) uniqueness of Shannon decomposition and compression up to permutation of unique rows, but no induction argument is written. The subsequent sentence that redundancy can be removed by choosing \"any lexicographic ordering\" is the first and only mention of that rule, and no lexicographic labeling procedure is defined or used in the construction. In particular, the SU decomposition in the Appendix (Algorithm 1) assigns row labels by order of first appearance in a hash table, so two compressions of the same function can produce different representatives. Since the unique representative is the basis for calling Eq. (7) a canonical normal form, this gap is load-bearing, not cosmetic.","section":"Section III, Eq. (7)"},{"comment":"The central operational claim about CLEAN is asserted without proof. The sentence \"importantly, manipulations of BMPs that can be performed efficiently ... lead to matrix products that can be compressed into canonical form with a polynomial number of steps\" is not supported by any termination or complexity argument for the LTR/RTL sweep schedule. In particular, the text states that reaching canonical form requires at least one round of LTR-cleaning, but it does not prove that one LTR sweep after one RTL sweep always reaches a fixed point, nor does it bound the cost of the compression steps such as Eq. (27), which require detecting and removing duplicate rows. Because APPLY, RESTRICT, JOIN, COMPOSE, SWAP, and REORDER all route through CLEAN, a non-terminating or order-dependent CLEAN would invalidate the paper's claim that BMP operations are closed on a canonical representation. The proof may be quite possible, but it must be supplied.","section":"Section IV.A, Eqs. (25)-(33)"},{"comment":"The claim that the RTL sweep alone is sufficient to compress the direct-sum APPLY output is left unexplained and appears in tension with the note in Section IV.A.2 that canonical form requires at least one LTR-cleaning round. If the special structure of the direct-sum construction makes RTL cleaning sufficient, the reason should be stated explicitly; otherwise the reader cannot verify that the direct-sum method produces the same canonical representative as the direct-product method after CLEAN.","section":"Section IV.B.2, Eq. (41)"}],"minor_comments":[{"comment":"The label on the left-hand side of Eq. (16) reads M(1)(x2), but the variable being decomposed is x1; it should read M(1)(x1).","section":"Section II.A, Eq. (16)"},{"comment":"The assembled BMP for h(x) = \\bar{x2} x1 x0 is missing the overbar on x2 in the first matrix, and the lower row of the last matrix should be (\\bar{x0} x0) to match Eq. (20).","section":"Section II.A, Eq. (21)"},{"comment":"The example function is written as f(x2,x1,x0)=x0(x2∨x2x1), but the following paragraph says the function is g(x)∨h(x) with h=x2 x1 x0; presumably the intended expression is x0(x2∨\\bar{x2}x1).","section":"Section V, Eq. (63)"},{"comment":"There is a typo in \"the the bypassing of nodes in non-complete BDDs\" and in Section IV.B.2 \"the method based of direct products\" should read \"based on direct products.\"","section":"Section V"},{"comment":"The notation in the APPLY complexity discussion is slightly confusing: the subfunctions f(vi, x'i) and g(vi, x'i) use the same label vi for the fixed prefix, but the two BMPs may have different bond dimensions pi and qi; clarifying that vi ranges over all 2^(n-i) assignments would improve readability.","section":"Section VI.B, Eqs. (83)-(84)"}],"recommendation":"major_revision","confidential_remarks":"The manuscript's own admission of no killer application and its explicit equivalence to quasi-reduced BDDs mean the contribution is primarily representational. That is acceptable for a data-structure paper if the central claims are substantiated, but the current version leaves the canonicity and CLEAN-normalization proofs as assertions. I would advise asking the authors to provide a rigorous proof of the canonical-form claim (with an explicit labeling rule) and a termination/complexity analysis of CLEAN, and to clarify the RTL-sufficiency claim in the direct-sum APPLY. If those proofs are supplied, the paper could be acceptable; without them, the central claims are not verifiable. The relationship to quasi-reduced BDDs should also be stated more prominently in the abstract or introduction, since it is both the main correctness anchor and the main limitation on novelty."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read it. Here's the short version: the paper does what it says in the title, and the core normal-form construction is sound, but the CLEAN operation--the one that every other operation depends on--is asserted rather than proven. The paper should go to review, but the authors need to close that gap.\n\nWhat's actually new: a matrix-product representation of Boolean functions built from Shannon decomposition and row-switching matrices, with a normal form that is unique up to row/column permutations and pinned down by a lexicographic ordering convention. The explicit translation to quasi-reduced BDDs is the clearest part of the paper and tells the reader exactly what the representation is: the same thing as reduced ordered BDDs with level padding and merging, dressed in linear algebra. The operation set (APPLY, RESTRICT, JOIN, COMPOSE, SWAP, REORDER) mirrors Bryant's BDD operations and is worked through in enough detail for an implementer to reproduce it. There is also a public Julia library, which is real evidence that the authors build what they describe.\n\nThe honest admission in Sec. VII that no killer application has been identified is a point in the paper's favor, not against it. The motive is practical--CUDD is hard to extend--and the linear-algebra framing could genuinely make a more accessible library.\n\nNow the soft spots. The stress-test note targets CLEAN, and it lands. The paper asserts that efficiently constructed matrix products can be compressed to canonical form in polynomial time, but there is no termination proof for the LTR/RTL sweep schedule and no complexity bound stated in terms of input and output size. The SU decomposition in the Appendix labels unique rows by first appearance in a hash table, which is not the lexicographic ordering used in the uniqueness claim, so even a fixed point of CLEAN is only well-defined up to permutations unless more is said. That is a real gap in the manipulation machinery. It does not undermine the existence of the normal form, which is built directly in Secs. II-III; it undermines the completeness of the operation set. A referee should ask for a precise statement about CLEAN's termination and the row-labeling convention.\n\nThe typos in Eqs. (16) and (21) are minor. The variable-order complexity discussion is standard and correctly attributed.\n\nBottom line: if you work with BDDs, tensor trains, or circuit representations, this is worth reading and discussing. It is not a breakthrough--it translates an existing data structure into matrix language--but the translation is competent and the operation set is useful. I would send it to a serious referee with a request to tighten CLEAN.","headline":"A creditable, clearly written paper that recasts quasi-reduced BDDs as a matrix product normal form; the core construction is sound, but the CLEAN operation on which all the manipulations rely is asserted rather than proven.","tokens_in":23973,"tokens_out":3741,"would_cite":false,"duration_ms":37553,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["06E30","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"For a fixed order of the Boolean variables, every vector of Boolean functions has a unique compressed representation as a product of binary matrices, and that representation converts losslessly to and from a binary decision diagram.","keywords":["Boolean functions","matrix product states","tensor trains","binary decision diagrams","normal form","Shannon decomposition","variable ordering","bond dimension"],"falsifier":"Run CLEAN on a family of n-bit Boolean networks whose BDDs are known to be polynomial; if the number of compression sweeps or intermediate matrix sizes grows faster than polynomial in n, the claimed canonicalization efficiency fails. More directly, exhibit one BMP that CLEAN reduces to two different row-switching forms under the same lexicographic rule, which would refute uniqueness.","tokens_in":22994,"feed_emoji":"🧮","tokens_out":5741,"duration_ms":56818,"temperature":0.7,"pith_summary":"The paper introduces a way to store Boolean functions as a train of binary matrices, one matrix per input variable, called a Binary Matrix Product (BMP). It claims that when the train is fully compressed, the representation is canonical: for a fixed order of the variables, the same function always yields, up to permuting rows and columns, the same BMP. Because the matrices are just 0/1 tables with one 1 per row, building and manipulating BMPs reduces to elementary linear algebra, and every BMP can be converted losslessly into a Binary Decision Diagram and back. The point of the representation is practicality: Boolean reasoning tools that rely on simple matrix operations rather than the intricate pointer machinery of decision-diagram libraries, with complexity controlled by reordering the variables.","feed_headline":"Matrix-product trains give Boolean functions a canonical form","feed_subtitle":"Compressed, the representation is unique per variable order and swaps losslessly with binary decision diagrams.","key_machinery":"The central object is the matrix train of row-switching matrices. Each $M^{{(i)}}$(x_i) has entries that are 0 or 1 with exactly one 1 per row, so it selects, for each subfunction carried on the left, which subfunction to carry on the right after fixing x_i. The terminal vector R=(0,1)^T encodes the two constant functions. The argument is carried by the CLEAN operation: a left-to-right sweep applies Shannon decomposition and removes duplicate rows, and a right-to-left sweep merges isomorphic terminal subgraphs; iterated, these sweeps produce the unique compressed form. The SWAP operation, based on two-sided Shannon decomposition, lets one reorder adjacent variables, and REORDER composes swaps; exact and heuristic search (A* with branch and bound, and sifting) minimize the accumulated bond dimension.","core_discovery":"For a vector of m Boolean functions on n variables, the paper constructs a representation F(x) = $M^{{(n-1)}}$(x_{n-1}) ... $M^{{(0)}}$(x_0) R, where each M is a row-switching matrix (one 1 per row) built by Shannon-decomposing on one variable and then deleting duplicate rows. The claim is that this construction, with duplicate rows removed at each stage, is a normal form: Eq. (7) is unique up to permutations of rows and columns, which the paper describes as a gauge freedom removable by lexicographic ordering. The CLEAN operation, sweeping left-to-right and right-to-left, restores canonical form after arbitrary manipulations, and the paper shows how to implement Boolean operations (APPLY, RESTRICT, INSERT, JOIN, COMPOSE, SWAP, REORDER) on BMPs. It also establishes the exchange: a BMP becomes a BDD by taking each matrix as the adjacency table between consecutive variable levels, and a BDD becomes a BMP after pass-through padding; maximally compressed BMPs correspond to quasi-reduced BDDs. The paper therefore claims not only a new normal form but a genuine equivalent pipeline to BDD-based reasoning carried by linear algebra.","pith_inferences":["A testable extension the paper leaves implicit: because BMP volume equals the node count of the equivalent quasi-reduced BDD up to padding, lower-bound techniques for BDD size should transfer to BMP bond dimension.","The MPS analogy suggests an approximate variant the paper does not pursue: truncating bond dimension during CLEAN would give a controlled approximation of a Boolean function, trading exactness for compactness.","If CLEAN is confirmed polynomial, practical significance depends on the empirical distribution of bond dimensions over typical circuits; a benchmark against BDD libraries on adder, multiplier, and netlist families would settle the practicality question.","The row-switching array representation makes BMPs naturally sparse, so software built on tuple arrays rather than full matrices may inherit the performance profile of adjacency-list BDD packages."],"forward_implications":["For a fixed variable order, two syntactically different BMPs that compute the same functions will compress to the same canonical form, so equivalence checks become a matter of compression.","Every operation available on BDDs, including apply, restrict, compose, and variable reordering, has a counterpart implemented on BMPs, so BDD-based reasoning can in principle run on a linear-algebra engine.","When the bond dimension stays polynomial in n, BMP evaluation and manipulation are polynomial, and this volume measure mirrors the node count of the equivalent quasi-reduced BDD.","The variable-ordering problem is inherited from BDDs: finding an order with small BMP volume is NP-complete, but exact A* search and sifting heuristics transfer directly.","The reversible-circuit and quantum-circuit verification settings that motivate the work are targets where the MPS/tensor-train analogy may bring tensor-network compression tools to Boolean reasoning."],"supporting_citations":[{"why":"Introduces the ordered BDD normal form and graph algorithms that the paper translates into and from BMPs.","marker":"[5]"},{"why":"Defines tensor-train decomposition, the object whose bond-dimension complexity BMPs mirror.","marker":"[35]"},{"why":"Formalizes matrix product states, the quantum many-body representation that motivates the BMP construction.","marker":"[37]"},{"why":"Shows the variable-ordering problem is NP-complete, a result the paper takes over for BMP volume minimization.","marker":"[3]"},{"why":"Supplies the exact A* with branch-and-bound search that the paper adapts to find minimum-volume variable orders.","marker":"[10]"},{"why":"Provides the sifting heuristic that the paper adapts for fast approximate variable reordering.","marker":"[39]"}],"fun_headline_variants":["Boolean functions meet tensor trains: a canonical matrix form","Matrix product state: a new normal form for Boolean logic","From BDDs to matrix trains: a canonical Boolean form","Shannon decomposition as matrix trains: canonical Boolean form","Matrix-product trains: the BDD's linear algebra twin"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the CLEAN operation always terminates in the unique compressed canonical form in polynomial time; the paper states this but gives no formal complexity bound or termination proof.","fun_headline_variants_meta":{"raw":{"variants":["Boolean functions meet tensor trains: a canonical matrix form","Matrix product state: a new normal form for Boolean logic","From BDDs to matrix trains: a canonical Boolean form","Shannon decomposition as matrix trains: canonical Boolean form","Matrix-product trains: the BDD's linear algebra twin"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000922,"raw_usage":{"total_tokens":4031,"prompt_tokens":1098,"completion_tokens":2933,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":714,"completion_tokens_details":{"reasoning_tokens":2853}},"tokens_in":714,"tokens_out":2933,"duration_ms":18991,"temperature":1.0,"reasoning_tokens":2853,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T04:06:05.181458+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run CLEAN on a family of n-bit Boolean networks whose BDDs are known to be polynomial; if the number of compression sweeps or intermediate matrix sizes grows faster than polynomial in n, the claimed canonicalization efficiency fails. More directly, exhibit one BMP that CLEAN reduces to two different row-switching forms under the same lexicographic rule, which would refute uniqueness.","supporting_citations":[{"cited_title":"In this formulation, a state q is a subset of the input variables Xn ={x1,x 2,...,x n}, representing all BMPs whose first|q| variables are those in q, in any order","cited_arxiv_id":null,"evidence_quote":"Introduces the ordered BDD normal form and graph algorithms that the paper translates into and from BMPs."},{"cited_title":"Michael Miller and Mitchell A","cited_arxiv_id":null,"evidence_quote":"Defines tensor-train decomposition, the object whose bond-dimension complexity BMPs mirror."},{"cited_title":"Novikov, M","cited_arxiv_id":null,"evidence_quote":"Formalizes matrix product states, the quantum many-body representation that motivates the BMP construction."},{"cited_title":"The canonical form for h(f,g ) is then obtained by applying the CLEAN operation to the resulting BMP of Eq","cited_arxiv_id":null,"evidence_quote":"Shows the variable-ordering problem is NP-complete, a result the paper takes over for BMP volume minimization."},{"cited_title":"Quantum supremacy using a programmable superconducting processor","cited_arxiv_id":null,"evidence_quote":"Supplies the exact A* with branch-and-bound search that the paper adapts to find minimum-volume variable orders."},{"cited_title":"Breadth-first manipulation of SBDD of boolean functions for vector processing","cited_arxiv_id":null,"evidence_quote":"Provides the sifting heuristic that the paper adapts for fast approximate variable reordering."}],"review_version":1}