{"id":"079efb53-0dee-4b7b-8e34-5e9db5de9762","arxiv_id":"1908.03252","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"An ADD-based symbolic Ryser algorithm computes permanents of dense and similar-row matrices up to size 70-80, outperforming CNF-based exact counters and explicit Ryser on these instances.","lead":"This paper presents a symbolic algorithm for computing exact matrix permanents using Algebraic Decision Diagrams (ADDs) to run Ryser's formula on compressed matrices. It reports that this approach solves dense and similar-row matrices of size up to 70-80 within 30 minutes, where current exact model counters and explicit Ryser time out.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The dense-matrix claim rests on benchmarks that are actually similar-row matrices, so the advertised dense-matrix result is unsupported.","rationale":"The reader's weakest assumption correctly identifies the benchmark-generation issue as the most load-bearing problem. My independent reading of Section 5.3 and Table 1 confirms that the dense family is generated by perturbing the all-ones matrix by O(n) flips, so every tested dense instance is also a similar-row instance. The similar-row experiments in Section 6.4 independently show scaling to n=80, which is consistent with this interpretation. The theory in Section 4 explicitly explains why identical or nearly identical rows yield compact ADDs, so the observed dense performance is the expected behavior of the similar-row mechanism rather than evidence about arbitrary dense matrices. I did not find a more severe internal flaw: Algorithm RysersADD is a correct symbolic implementation of Ryser's formula, the early-abstraction rule in Theorem 1 is valid, and the paper honestly states that the ADD-succinctness characterization is open. The missing code release and fixed-seed details are secondary reproducibility concerns. Given that the headline claim about dense matrices is not supported by the current experiments, the appropriate verdict is CONDITIONAL rather than ACCEPT: the paper should either add Bernoulli-style independent dense matrix experiments or explicitly restrict its claim to dense matrices with similar rows.","tokens_in":15088,"tokens_out":2256,"duration_ms":24741,"concrete_test":"Generate 20 independent Bernoulli(p) n x n 0-1 matrices for each p in {0.3, 0.5, 0.7, 0.9} and each n in {30, 40, 50}, using a fixed seed, and run RysersADD and RysersADD-P with the same Sylvan settings, a 42 GB memory cap, and an 1800 s timeout. Report median wall time, number of timeouts, and maximum ADD node count for each (p, n) cell, and compare against Section 6.2's dense curves. If the Bernoulli instances time out or exhibit ADD sizes growing close to 2^n while the Section 5.3 benchmarks scale, the dense-matrix claim must be narrowed to 'dense matrices with nearly identical rows'.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The central empirical claim, that the frontier of practically efficient permanent computation is pushed to dense matrices, depends on Section 5.3's dense benchmark being representative of dense matrices. It is not. Table 1 generates a 'dense' instance by starting from the all-ones matrix and flipping at most Cf·n entries with Cf <= 1.4. For n=70 this changes at most 98 of 4900 entries, i.e., at most 2% of the matrix. The resulting matrix is Hamming-close to all-ones, and its rows are almost identical to one another; this is precisely the 'similar rows' class that Section 4's ideal identical-row example motivates. The n=70 dense successes in Section 6.2 therefore demonstrate scalability on near-identical-row matrices, not on arbitrary dense matrices. The abstract and Section 1 advertise dense matrices as a separate class achieved, but no experiment uses matrices with independent random entries such as Bernoulli(0.5) matrices, where row sums and the ADD structure are not governed by near-identity with all-ones. The paper itself notes in Section 7 that a complete characterization of matrices with compact ADDs is open, which makes the missing control on arbitrary dense inputs more significant. The algorithm's correctness is not in doubt, and the similar-row result is supported, but the 'dense matrices' portion of the strongest claim outruns the evidence.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents RysersADD, an exact algorithm for computing the permanent of a 0-1 matrix by translating Ryser's formula into operations on Algebraic Decision Diagrams (ADDs). Row sums are represented as ADDs, multiplied with a parity ADD, and the permanent is obtained by additively quantifying out all column variables. An early-abstraction step, taken from the ADDMC weighted model counter, allows variables to be eliminated as soon as they no longer occur in future factors. The authors report experiments on random sparse, dense, and 'similar-row' matrices (generated by flipping O(n) entries of an all-zero, all-one, or repeated-row starting matrix), plus SuiteSparse and fullerene instances. RysersADD and the parallel version RysersADD-P solve dense instances up to n=70 and similar-row instances up to n=80 within 1800 seconds, while explicit Ryser and the model counters D4 and DSharp time out earlier. The paper concludes that the frontier of practical permanent computation is pushed beyond sparse matrices to dense and similar-row matrices.","tokens_in":15289,"tokens_out":7949,"duration_ms":78540,"significance":"The algorithmic idea is clean and exact: it is a direct symbolic execution of Ryser's formula with no fitted parameters, and the early-abstraction theorem from ADDMC is used as a proven building block. The experimental study is broad in its coverage of baselines (explicit Ryser, D4, DSharp with six encodings) and benchmark families, and the similar-row results are genuinely interesting. If the dense-matrix claim were supported, this would be a notable practical advance. However, the dense benchmark design conflates density with row-similarity, so the evidence does not support the advertised 'dense matrices' contribution. The work is best read as evidence for scalability on matrices whose rows are mutually close, including near-all-ones matrices, not on arbitrary dense matrices.","major_comments":[{"comment":"The 'dense' benchmark family is generated by starting from the all-ones matrix and flipping at most Cf·n entries, with Cf ≤ 1.4. For n=70 this changes at most 98 of 4900 entries (2%), so the resulting rows differ from the all-ones row in only a few positions and are nearly identical to one another. These instances are therefore a special case of the 'similar rows' class the paper itself motivates in Section 4, and the scaling in Figure 3 does not demonstrate scalability on arbitrary dense matrices, such as independent Bernoulli(0.5) matrices. Since the abstract and Section 1 claim that the frontier is pushed 'to the classes of dense matrices,' this claim outruns the evidence; the authors should either add experiments on genuinely random dense matrices or explicitly restrict the conclusion to near-all-ones / row-similar matrices.","section":"5.3 (Table 1), 6.2 (Fig. 3)"},{"comment":"The paper's central contribution claim is that the frontier of practically efficient permanent computation is pushed to dense matrices. Yet no experiments are reported on matrices with independent random entries, and Section 7 concedes that a complete characterization of matrices admitting compact ADDs is open. Given these gaps, the broad 'dense matrices' claim is not established by the presented evidence. The revision should either provide control experiments with, e.g., Bernoulli(0.5) dense matrices, or explicitly narrow the scope of the contribution to matrices that are close (in Hamming distance) to a common row, and adjust the abstract and introduction accordingly.","section":"Section 1 and Section 7"}],"minor_comments":[{"comment":"The description of Servedio and Wan's result as applying to 'matrices with at most C·n zeros' appears to be incorrect; the original result concerns matrices with at most C·n nonzeros (i.e., few ones). Please correct this to avoid misrepresenting the related work.","section":"Section 3"},{"comment":"The word 'Westemere' appears to be a typo; it should likely be 'Westmere'.","section":"Section 5.2"},{"comment":"The text says 'despite the density of 1s being 9n' for the instance can_61. Since 9n is a count rather than a density, the wording should be changed to 'the number of 1s being 9n'.","section":"Section 6.5"},{"comment":"The statement that the monolithic approach is used for dense and similar-row cases should be made explicit in the captions of Figures 3 and 5, so readers know whether the plotted times use early abstraction or not.","section":"Section 5.1"},{"comment":"The row labels 'Encoding / Mode 1 2 3 4 5 6 EA Mono EA Mono' are hard to parse; please clarify which columns correspond to D4, DSharp, and the RysersADD variants.","section":"Section 6.6, Table 2"},{"comment":"The scatter plots include only instances that did not time out; this selection should be stated in the caption, as it can bias the perceived correlation between ADD size and runtime.","section":"Section 6.1, Fig. 2"}],"recommendation":"major_revision","confidential_remarks":"The main concern is the representativeness of the 'dense' benchmark. The algorithm's correctness and the similar-row results are solid, but the headline claim about dense matrices will need either new experiments or a substantially more cautious statement. I do not see a circularity problem; the method is an exact translation of Ryser's formula and the early-abstraction theorem is cited properly as prior work."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe useful thing in this paper is the algorithm itself: Ryser's formula evaluated on ADDs with early abstraction. That combination is new as far as the citations show, the correctness argument is a direct translation of Ryser's identity, and the engineering is solid. The experiments are careful: 2125 instances, well over 2500 hours of compute, with comparisons against explicit Ryser, D4, DSharp under six encodings, and ADDMC. On matrices whose rows are close to identical, and on a few structured graphs (can_61, C60), RysersADD is genuinely competitive or better. The scatter plots of ADD size versus runtime support the claimed connection between diagram compactness and speed. I buy the core story: for matrices that admit a compact ADD, this is a practical way to push exact permanents well beyond n≈35.\n\nThe soft spot is the dense-matrix claim. The 'dense' benchmark family is generated by starting from the all-ones matrix and flipping at most 1.4n entries (Section 5.3). For n=70 that is at most two percent of the entries. These matrices are dense in the literal sense, but they are also near-identical-row matrices, and the paper itself says in Section 4 that dense matrices can be thought of as starting from all ones and changing a few entries. So the abstract's separation of 'dense' from 'similar rows' is not supported by the data. There are no experiments on arbitrary dense matrices, e.g., Bernoulli(0.5), where ADD blow-up is plausible. The conclusion hedges by noting that a complete characterization is open, but the abstract and introduction make a stronger claim than the evidence carries. This is addressable: narrow the claim or run the missing benchmarks. The absence of released code and instance-level data also makes the exact numbers hard to verify, though the generator parameters are described precisely enough that reproduction is possible.\n\nI do not see this as fatal. The algorithm is exact, the similar-row and structured results stand, and the paper is honest about the open characterization. It deserves a serious referee. My recommendation: engage with it, but push on the benchmark question and ask for the tool to be released.","headline":"Clean symbolic-Ryser algorithm with real promise on structured matrices, but the 'dense' claim is supported only by near-all-ones benchmarks and needs tightening.","tokens_in":15852,"tokens_out":3679,"would_cite":true,"duration_ms":37190,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Computing a matrix permanent is usually practical only for sparse matrices; this paper shows that a symbolic version of Ryser's formula, built on Algebraic Decision Diagrams, computes exact permanents of dense 70x70 and similar-row 80x80…","keywords":["matrix permanent","algebraic decision diagrams","Ryser's formula","symbolic computation","exact counting","perfect matchings","0-1 matrices","early abstraction"],"falsifier":"Run the proposed algorithm on random 0-1 matrices of size $n=40$ or $n=50$ in which each entry is independently 1 with probability 0.5, recording the maximum ADD node count and wall-clock time, and compare with the flipped-from-all-ones instances of the same size. If the ADD size jumps to millions of nodes or the run exceeds the 1800-second timeout even at $n=40$, the dense-matrix conclusion does not extend to arbitrary dense inputs; if it completes quickly, the claim is strengthened.","tokens_in":14832,"feed_emoji":"🧮","tokens_out":12904,"duration_ms":120967,"temperature":0.7,"pith_summary":"The paper asks whether exact computation of the matrix permanent, a #P-complete problem usually tackled only for sparse inputs, can be pushed to dense and row-similar matrices. It answers yes: encode the matrix as an Algebraic Decision Diagram and run Ryser's inclusion-exclusion formula symbolically, letting the diagram share repeated partial computations. The experiments show exact permanents of $70\\times 70$ dense 0-1 matrices and $80\\times 80$ matrices with almost identical rows computed within 1800 seconds; in the same setting the explicit Gray-code implementation of Ryser's algorithm times out for $n\\ge 34$, while the compared SAT-based counters time out on all dense instances of size 30 and all similar-row instances of size 40. The message is that compact symbolic representation, not sparsity alone, is a workable route to practical permanent computation.","feed_headline":"Decision diagrams push exact permanents to dense 70x70 matrices","feed_subtitle":"The symbolic algorithm also solves similar-row 80x80 matrices, far beyond explicit Ryser and SAT counters.","key_machinery":"The central object is the Algebraic Decision Diagram (ADD), a directed acyclic graph representing a real-valued function of Boolean variables by sharing identical substructures. Here the Boolean variables say whether a column belongs to the subset $S$ in Ryser's formula; the ADD's leaves carry integer values such as row sums, products, and the parity sign $(-1)^{|S|}$. The diagram does the work: when rows are identical or similar, the row-sum ADDs are isomorphic and merge, and memoization through shared nodes avoids recomputing the same partial sums. The supporting mechanism is early abstraction, the identity $\\exists x\\,(f\\cdot g)=(\\exists x\\,f)\\cdot g$ when $x$ does not occur in $g$, which lets the algorithm quantify out column variables as soon as they are irrelevant, keeping the diagram small. The experiments show a strong correlation between ADD node count and running time, confirming that diagram size is the operative resource.","core_discovery":"The central discovery is that a symbolic implementation of Ryser's formula, built on Algebraic Decision Diagrams and driven by early abstraction, opens a practical frontier beyond sparse matrices. For an $n\\times n$ 0-1 matrix the paper represents, as an ADD, the function $(-1)^{|S|}\\prod_{i=1}^{n}\\sum_{j\\in S}a_{i,j}$ on subsets $S$ of columns; the permanent is obtained by adding the values over all $S$. Row sums for similar rows become shared subgraphs, so the diagram stays small exactly when rows are near-identical; early abstraction then eliminates a column variable as soon as no remaining row-sum factor depends on it. On 2125 generated benchmarks, exact permanents are reported for dense matrices up to $n=70$ and similar-row matrices up to $n=80$ within 1800 seconds, whereas the explicit implementation of Ryser's formula times out for $n\\ge 34$ and neither SAT-based counter can solve the smallest dense or similar-row instances tested. The authors present this as first evidence that the frontier of practically efficient permanent computation can be pushed well beyond sparse matrices.","pith_inferences":["Editorial inference: the dense benchmarks are built by flipping at most $1.4n$ entries of the all-ones matrix, so every row remains close to every other; arbitrary dense matrices, such as independent random entries with density 0.5, may not admit compact ADDs and are not covered by the experiments.","Editorial inference: the same ADD-plus-early-abstraction recipe could be applied to other subset-sum factorizations, such as counting Hamiltonian cycles or monomer-dimer partition functions, whenever the summed quantity factorizes row-wise and rows repeat structure.","Editorial inference: the correlation between ADD size and running time suggests a testable design principle - row ordering and clustering that maximize shared subgraphs should transfer to other decision-diagram libraries and to weighted model counting.","Editorial inference: a complete characterization of matrices with succinct ADD representations would let the approach yield theoretical upper bounds for dense matrices analogous to the earlier sparse-matrix bounds, a direction the authors leave open."],"forward_implications":["Exact permanent computation becomes practical for dense 0-1 matrices up to at least $n=70$, roughly double the limit of the explicit implementation of Ryser's formula used in the comparison.","Matrices whose rows differ in only a few positions can be solved up to $n=80$, with performance degrading gracefully as row similarity decreases.","With early abstraction, the same symbolic algorithm remains competitive with SAT-based counters on sparse matrices and outperforms them as density grows.","ADD size is the predictive resource: instances with compact diagrams run quickly, so heuristics that maximize subgraph sharing should be the focus of further work."],"supporting_citations":[{"why":"Defines Algebraic Decision Diagrams, the data structure on which the symbolic Ryser algorithm is built.","marker":"[3]"},{"why":"Supplies the early-abstraction theorem and the clustering heuristics the algorithm uses to keep ADD size small and to handle sparse instances.","marker":"[20]"},{"why":"Gives Ryser's formula, the inclusion-exclusion identity the algorithm turns into a decision-diagram computation.","marker":"[47]"},{"why":"Provides the explicit Gray-code implementation of Ryser's algorithm used as the baseline that times out for matrices of size 34 and larger.","marker":"[39]"},{"why":"The SAT-based exact model counter used as a comparison baseline; it times out on dense and similar-row instances.","marker":"[34]"},{"why":"The other compared SAT-based model counter, generally outperformed by the ADD-based method.","marker":"[38]"},{"why":"Proves that computing the 0-1 permanent is #P-complete, motivating the search for practical subclasses.","marker":"[55]"},{"why":"Supplies the multi-core ADD library with arbitrary-precision arithmetic used to implement and parallelize the algorithm.","marker":"[56]"},{"why":"Represents the earlier sparse-matrix algorithmic advances that the paper aims to move beyond.","marker":"[49]"}],"fun_headline_variants":["ADDs compute exact permanents for dense 70x70 matrices","Symbolic Ryser cracks dense 70 and similar-row 80 exactly","Exact permanents: ADDs go beyond sparse to dense 70","ADD-based Ryser beats sparse limit: dense 70 solved","With ADDs, exact permanents reach dense 70x70"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the matrices used for the dense case, generated by flipping a few entries of the all-ones matrix, stand in for dense matrices as a class; if arbitrary dense 0-1 matrices make the decision diagram grow explosively, the main claim about dense matrices would not be supported.","fun_headline_variants_meta":{"raw":{"variants":["ADDs compute exact permanents for dense 70x70 matrices","Symbolic Ryser cracks dense 70 and similar-row 80 exactly","Exact permanents: ADDs go beyond sparse to dense 70","ADD-based Ryser beats sparse limit: dense 70 solved","With ADDs, exact permanents reach dense 70x70"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000643,"raw_usage":{"total_tokens":3005,"prompt_tokens":1039,"completion_tokens":1966,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":655,"completion_tokens_details":{"reasoning_tokens":1874}},"tokens_in":655,"tokens_out":1966,"duration_ms":13141,"temperature":1.0,"reasoning_tokens":1874,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:19:33.060762+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the proposed algorithm on random 0-1 matrices of size $n=40$ or $n=50$ in which each entry is independently 1 with probability 0.5, recording the maximum ADD node count and wall-clock time, and compare with the flipped-from-all-ones instances of the same size. If the ADD size jumps to millions of nodes or the run exceeds the 1800-second timeout even at $n=40$, the dense-matrix conclusion does not extend to arbitrary dense inputs; if it completes quickly, the claim is strengthened.","supporting_citations":[{"cited_title":"Bahar, E","cited_arxiv_id":null,"evidence_quote":"Defines Algebraic Decision Diagrams, the data structure on which the symbolic Ryser algorithm is built."},{"cited_title":"ADDMC: Weighted Model Counting with Algebraic Decision Diagrams","cited_arxiv_id":"1907.05000","evidence_quote":"Supplies the early-abstraction theorem and the clustering heuristics the algorithm uses to keep ADD size small and to handle sparse instances."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives Ryser's formula, the inclusion-exclusion identity the algorithm turns into a decision-diagram computation."},{"cited_title":"Nijenhuis and H","cited_arxiv_id":null,"evidence_quote":"Provides the explicit Gray-code implementation of Ryser's algorithm used as the baseline that times out for matrices of size 34 and larger."},{"cited_title":"Lagniez and P","cited_arxiv_id":null,"evidence_quote":"The SAT-based exact model counter used as a comparison baseline; it times out on dense and similar-row instances."},{"cited_title":"Muise, S","cited_arxiv_id":null,"evidence_quote":"The other compared SAT-based model counter, generally outperformed by the ADD-based method."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Proves that computing the 0-1 permanent is #P-complete, motivating the search for practical subclasses."},{"cited_title":"van Dijk and J","cited_arxiv_id":null,"evidence_quote":"Supplies the multi-core ADD library with arbitrary-precision arithmetic used to implement and parallelize the algorithm."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Represents the earlier sparse-matrix algorithmic advances that the paper aims to move beyond."}],"review_version":1}