{"id":"42a2285e-41b5-49af-a027-962f7b72a8a5","arxiv_id":"2412.14933","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Cirbo is a new open-source tool whose hybrid SAT-based synthesis and minimization methods produced the smallest known circuits for many IWLS 2024 benchmarks.","lead":"The paper presents Cirbo, an open-source Python tool for Boolean circuit synthesis and minimization, and reports that it won the IWLS 2024 Programming Contest. It shows size reductions of up to 83 percent on benchmark circuits compared to the best 2023 contest entries.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The paper's headline 12% average-reduction statistic is not verifiable from the paper itself, because the benchmark set over which the average is taken and the full per-benchmark results are omitted; this is the most load-bearing gap.","rationale":"The strongest claim has two parts: winning the competition and reducing the best 2023 circuits by 12% on average. The winning claim is supported by the contest result and by the open-source code, but the reduction claim is the load-bearing numerical headline. The paper presents only selected examples, all with positive improvements, and never provides the full per-benchmark distribution or the exact set over which the average is computed. The described comparison-subtraction subcircuit is underspecified and potentially worrying, but a standard ripple subtractor can indeed be built with size 5 per bit in an XAIG basis, and the open-source repository makes it directly checkable. Thus the more serious blocker for the central claim is the missing aggregate evidence. My recommendation remains CONDITIONAL, matching the reader: the paper should be accepted only if the missing benchmark data and scripts are supplied or the claims are narrowed. I partially agree with the reader because they also mention the missing distribution in the rationale, but their weakest_assumption focuses on the arithmetic subcircuit, which I regard as a secondary and testable issue.","tokens_in":10416,"tokens_out":8250,"duration_ms":71164,"concrete_test":"Download the Cirbo repository and the official IWLS 2024 benchmark list; locate or reconstruct the exact generation and minimization scripts used to produce the submitted circuits for all 100 functions, and obtain the official IWLS 2023 best sizes for the same functions. Run the published pipeline and compute the mean percentage size reduction over the complete set. If the mean (or the official contest aggregation) differs materially from 12%, or if the scripts and baseline data are absent from the repository, the abstract's headline claim should be revised or explicitly qualified.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is the empirical claim that Cirbo reduces the size of the best IWLS-2023 circuits by 12% on average, with up to 83% reduction. Table 1 is explicitly a 'selection' of benchmarks, and Tables 4-6 cover only MAJ, SORT, and neuron functions. The text promises 'more statistics,' but the full distribution over the 100 contest functions, including zero and negative improvements, is not given; the paper also never states whether the 12% is an arithmetic mean over all 100 functions, over both bases, or over only the functions that improved. Without the full distribution and the official 2023 baseline sizes, the aggregate number cannot be checked. The reader's concern about the 5(n-i) comparison-subtraction subcircuit is legitimate but less load-bearing: it is a local claim about one arithmetic construction, and it can be checked directly against the open-source code; the headline statistic, by contrast, is the paper's primary contribution and is currently unsupported by the data presented.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces Cirbo, an open-source Python tool for Boolean circuit analysis, synthesis, and minimization. It describes features for function/circuit analysis, SAT-based exact synthesis, local minimization, and a database of near-optimal circuits for small functions. The authors report results on IWLS 2024 contest benchmarks, claiming a 12% average reduction over the best IWLS 2023 circuits, with individual reductions up to 83%, and state that the tool won the IWLS 2024 Programming Contest. They also outline techniques for arithmetic functions, symmetric functions (SUM, MAJ, SORT), and minimization of existing circuits such as neuron benchmarks.","tokens_in":10608,"tokens_out":2213,"duration_ms":19808,"significance":"If the headline empirical claims are correct, Cirbo is a leading practical tool for Boolean circuit minimization, and the paper would document substantial progress on well-studied benchmark families. The tool is open source, the code snippets are concrete, and several claims (e.g., the 5(n-i) comparison-subtraction construction for division) are checkable against the released code. The reported improvements on specific arithmetic, symmetric, and neuron functions are plausible and interesting. However, the central aggregate claim—the 12% average reduction—is not backed by the data presented in the paper, and the comparison to existing tools is asserted rather than demonstrated.","major_comments":[{"comment":"The headline claim that Cirbo 'reduce[s] the size of the best circuits from 2023 by 12% on average' is not verifiable from the paper. Table 1 shows only a 'selection' of eight benchmarks, and Tables 4–6 cover only MAJ, SORT, and neuron functions. The paper never states the full distribution over the 100 contest functions, does not give the IWLS 2023 baseline sizes for all benchmarks, and does not define the exact average (arithmetic mean over all 100 functions in each basis, over both bases combined, or over only improved functions). Since the 12% figure is the paper's central quantitative contribution, it must be supported by a complete table or supplementary data.","section":"Abstract and Experimental Evaluation, Table 1"},{"comment":"The claim that 'one can combine the comparison and the subtraction in the same subcircuit of size 5(n-i)' is load-bearing for the reported DIV and MOD improvements (for example, the 44% reduction on div8 in Table 1), but no construction or proof is given. The text describes processing bits from least significant to most significant and applying a Full Adder, yet the claimed size bound and the correctness of the combined operation are not derived. Either a detailed circuit construction with an induction argument or an exact reference to the code location and a machine-checkable proof should be provided.","section":"Arithmetic Functions, DIV construction"},{"comment":"The paper states that 'as our experiments show, our tool is capable of solving various datasets better than the tools mentioned above' (ABC, mockturtle, CLI, CIOPS), but no experimental comparison against these tools is presented anywhere in the manuscript. This claim is important because it positions Cirbo relative to the state of the art, and it is not supported by any table, figure, or protocol description. The authors should either add such a comparison or explicitly limit the claim to the contest benchmarks and to the combined workflow that uses ABC and CIOPS.","section":"Related Work and Experimental Evaluation"},{"comment":"The introduction promises 'more statistics as well as detailed steps that led to improved circuits,' but the full statistics are not included in the paper. In particular, the database section (Table 2) reports that for AIG some classes have circuits without a proof of optimality, yet the text says 'the vast majority of them are provably optimal' without quantifying which portion is proved. This ambiguity should be resolved by stating the exact number or fraction of functions with proofs for each basis.","section":"Introduction and Database section"}],"minor_comments":[{"comment":"The phrase 'the focus of the this paper' contains a typo; it should read 'the focus of this paper.'","section":"Introduction"},{"comment":"The benchmark column mixes informal descriptions (e.g., 'modulo8') with IWLS codes (ex33) without formally defining all listed functions; the text later defines many functions but not 'modulo8' and 'espresso' explicitly.","section":"Table 1"},{"comment":"The statement that a gate can compute any unary or binary Boolean function is immediately followed by the equivalence to XOR/AND/NOT, but the notation B2 \\ {⊕, ≡} is introduced without a definition of ≡ as equivalence; this may confuse readers unfamiliar with the convention.","section":"Boolean Circuits"},{"comment":"The function name 'minimize subcircuits' in Listing 10 appears with an underscore in the code snippet ('minimize_subcircuits') but is described in prose as 'minimize subcircuits'; the tool should use a consistent identifier.","section":"Minimization"},{"comment":"The database section states that classification 'considers the permutation of outputs' but does not describe how many equivalence classes were obtained or how the representatives were chosen; a brief algorithmic description would improve reproducibility.","section":"Database of (Nearly) Optimal Circuits"},{"comment":"Tables 4 and 5 report improvements as percentages, but for smaller values the difference is a few gates; the raw gate counts are given, which is good, but the reader should be told whether the percentages are rounded to the nearest integer or truncated.","section":"Experimental Evaluation, MAJ and SORT"}],"recommendation":"major_revision","confidential_remarks":"The paper is a tool paper whose main selling point is the contest result and the 12% average improvement, but the supporting data are incomplete in the current version. The authors should be asked to include the full per-benchmark table as supplementary material and to make the average definition explicit. The comparison-subtraction construction should also be documented, even if only in the appendix or via a formal statement with proof. The paper is likely fixable within revision, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: Cirbo is a genuinely useful open-source tool, and the concrete per-benchmark numbers in the tables look credible. The abstract's 12% average-reduction headline is not backed by the data presented in the paper, and the key 5(n-i) comparison-subtraction subcircuit is asserted without a construction. Both issues are fixable, and the paper deserves a serious referee.\n\nWhat's new and good: the tool itself is a real artifact, written in Python, open source, and it integrates SAT-based exact synthesis, local subcircuit minimization, NPN-style classification, and ABC/CIOPS calls. The database of provably optimal XAIG circuits and near-optimal AIG circuits for all functions with at most three inputs and three outputs is a solid, reproducible contribution; the XAIG side is formally grounded. The reported improvements on MAJ, SORT, and neuron benchmarks are concrete, with tables comparing 2023 and 2024 sizes. Winning the IWLS 2024 contest is an external validation that carries real weight. The division construction idea, combining comparison and subtraction, is interesting even though it is only sketched.\n\nSoft spots: first, the 12% average is the headline claim, but the paper gives only a selection in Table 1 plus tables for three function families. There is no full distribution over the 100 contest functions, no statement of whether the average is over functions, bases, or only the improved ones, and no zero or negative cases are shown. As written, that number cannot be independently checked. Second, the 5(n-i) subcircuit is described in one sentence with no circuit diagram or proof; if the bound is wrong or the construction is larger, the reported DIV and MOD gains would shrink. This is a local issue and likely verifiable against the open-source code, but the paper should include the construction or a proof. Third, the claim that Cirbo outperforms ABC, mockturtle, CLI, and CIOPS is stated without presenting any comparison data; that may live in the repository, but it is not in the paper.\n\nNone of these are fatal. The empirical core probably holds, since the contest result and the specific tables are hard evidence. What is missing is exactly what a referee should ask for: the full benchmark distribution and a detailed description of the arithmetic subcircuit.\n\nWho is this for: people working in logic synthesis, circuit minimization, SAT-based synthesis, and EDA tooling. It is not a theory paper; the value is in the artifact and the benchmark numbers. I would send it to review, conditional on the authors supplying the full data and clarifying the construction.","headline":"Solid tool paper with a real open-source artifact and credible per-benchmark gains, but the headline 12% average is underdocumented and the key arithmetic subcircuit claim needs a construction before the paper's central claims are fully checkable.","tokens_in":11175,"tokens_out":2714,"would_cite":true,"duration_ms":23127,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"An open-source tool for Boolean circuits cuts the size of the best-known circuits by 12% on average and up to 83%.","keywords":["Boolean circuits","circuit minimization","SAT-based exact synthesis","arithmetic circuits","circuit satisfiability","IWLS 2024 contest","AIG","XAIG"],"falsifier":"Build the claimed $5(n-i)$ comparison-subtraction block for $n=8$ and run an equivalence check against a separately constructed comparator-plus-subtractor; any mismatch, or any correct implementation requiring more than $5(n-i)$ gates, would refute the paper's division-circuit claim.","tokens_in":10238,"feed_emoji":"⚙️","tokens_out":6277,"duration_ms":49547,"temperature":0.7,"pith_summary":"Cirbo is presented as an open-source Python tool for analyzing, synthesizing, and minimizing Boolean circuits. The paper's central claim is that combining presynthesized arithmetic building blocks, SAT-based exact synthesis of small subcircuits, local subcircuit replacement, and a database of near-optimal small circuits yields smaller circuits than the best known results. On the IWLS 2024 contest benchmarks, the authors report an average size reduction of 12% against the best 2023 circuits, with individual reductions up to 83% on a modulo-8 circuit. If these results hold, Cirbo would currently be a leading practical tool for automatic circuit minimization, with consequences for hardware design and for experiments in circuit complexity.","feed_headline":"Open-source circuit tool cuts best sizes by 12%, up to 83%","feed_subtitle":"Cirbo wins IWLS 2024 by pairing SAT-based local minimization with arithmetic building blocks.","key_machinery":"The load-bearing mechanism is local SAT-based minimization: cut out a small subcircuit, compute the partial Boolean function it implements, ask a SAT solver for the smallest circuit computing that partial function, and swap it in if it is smaller, then iterate. Supporting this are a database of near-optimal circuits for every Boolean function with at most three inputs and three outputs, built using classification up to permuting and negating inputs and outputs, and the paper's new combined comparison-subtraction block of size $5(n-i)$, which lets each step of a grade-school division algorithm both test and update the remainder in one pass.","core_discovery":"At the core, the paper claims that practical Boolean circuit minimization can be pushed much further by treating circuits hierarchically: first build a structured circuit out of optimized blocks such as comparators, adders, and multipliers, then repeatedly replace small subcircuits by exact minimum-size circuits found via a SAT solver, guided by a precomputed database of provably optimal or near-optimal circuits for all functions with at most three inputs and three outputs. The key new arithmetic ingredient is a single subcircuit of size $5(n-i)$ that simultaneously compares and subtracts, which the paper says underlies its division and modulo improvements, including reductions of 44% to 84% over the 2023 best circuits. On the contest's AIG and XAIG bases, the tool produced the smallest circuit for more than half of the 100 functions.","pith_inferences":["If the $5(n-i)$ block stands, the grade-school division algorithm's circuit size is essentially pinned down near $4n^2$ in both bases, so further gains on division and modulo would have to come from a different algorithm, not tuning.","The same exact small-subcircuit replacement idea could be applied to cryptographic S-boxes or error-correcting decoding circuits, where local structure is less visible; no contest data supports this yet.","Since the database covers only three-input, three-output functions, scaling the exact-synthesis database to four-input functions might unlock further reductions, at the cost of much harder SAT instances.","The reported 83% reduction on modulo8 suggests that modulo arithmetic circuits had been far from optimized, so re-examining other modular arithmetic benchmarks with the same pipeline is a natural next test."],"forward_implications":["Any circuit family whose computation can be decomposed into small subcircuits can in principle benefit from the same local replacement loop, not just the contest benchmarks.","The reported arithmetic improvements imply that the 2023 contest circuits were substantially suboptimal for division, modulo, square, and square root, suggesting the same may hold for other arithmetic functions.","The open-source release lets other groups reproduce the contest results and apply the tool to new circuit design tasks.","For symmetric functions, the paper's recipe of compressing inputs with a SUM circuit and then synthesizing the output function on the compressed bits yields smaller circuits for MAJ and SORT."],"supporting_citations":[{"why":"Supplies the SAT-based exact synthesis method used to find minimum-size circuits for small blocks.","marker":"(Kojevnikov, Kulikov, and Yaroslavtsev 2009)"},{"why":"Provides the local subcircuit improvement loop and the exact-synthesis tool used to populate the optimal-circuit database.","marker":"(Kulikov, Pechenev, and Slezkin 2022)"},{"why":"General-purpose synthesis and minimization baseline that the tool is compared against and combined with.","marker":"(Brayton and Mishchenko 2010)"},{"why":"Gives the $4.5n+o(n)$ upper bound for SUM in XAIG, the target the tool's SUM generators aim at.","marker":"(Demenkov et al. 2010)"},{"why":"Shows how to convert circuits to CNF, the standard step used for satisfiability checking and SAT-based synthesis.","marker":"(Tseitin 1968)"},{"why":"SAT solver interface used by the tool's satisfiability and synthesis routines.","marker":"(Ignatiev, Morgado, and Marques-Silva 2018)"},{"why":"Supplies the classification approach that lets the database cover all 3-input, 3-output functions through representatives.","marker":"(Haaswijk et al. 2017)"},{"why":"Source of the 32 neuron benchmarks from the contest that the tool optimized.","marker":"(Umuroglu et al. 2020)"},{"why":"QBF-based exact synthesis tool used alongside Cirbo on neuron benchmarks.","marker":"(Reichl, Slivovsky, and Szeider 2023)"}],"fun_headline_variants":["Cirbo wins IWLS 2024, cuts circuit sizes by 83%","Hierarchical SAT minimization shrinks circuits up to 83%","Open-source Cirbo beats 2023 best circuits by up to 83%","New circuit tool wins IWLS 2024 with 12% average cut","Open-source tool beats DeepMind by 12% in circuit contest"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The paper asserts, without giving a construction or proof, that comparison and subtraction can be fused into one subcircuit of size exactly $5(n-i)$; if that block is incorrect or needs more gates, the reported division and modulo reductions would not hold.","fun_headline_variants_meta":{"raw":{"variants":["Cirbo wins IWLS 2024, cuts circuit sizes by 83%","Hierarchical SAT minimization shrinks circuits up to 83%","Open-source Cirbo beats 2023 best circuits by up to 83%","New circuit tool wins IWLS 2024 with 12% average cut","Open-source tool beats DeepMind by 12% in circuit contest"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000533,"raw_usage":{"total_tokens":2508,"prompt_tokens":836,"completion_tokens":1672,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":452,"completion_tokens_details":{"reasoning_tokens":1586}},"tokens_in":452,"tokens_out":1672,"duration_ms":10933,"temperature":1.0,"reasoning_tokens":1586,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T11:46:28.473366+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build the claimed $5(n-i)$ comparison-subtraction block for $n=8$ and run an equivalence check against a separately constructed comparator-plus-subtractor; any mismatch, or any correct implementation requiring more than $5(n-i)$ gates, would refute the paper's division-circuit claim.","supporting_citations":[{"cited_title":"S.; and Yaroslavtsev, G","cited_arxiv_id":null,"evidence_quote":"Supplies the SAT-based exact synthesis method used to find minimum-size circuits for small blocks."},{"cited_title":"S.; Pechenev, D.; and Slezkin, N","cited_arxiv_id":null,"evidence_quote":"Provides the local subcircuit improvement loop and the exact-synthesis tool used to populate the optimal-circuit database."},{"cited_title":"K.; and Mishchenko, A","cited_arxiv_id":null,"evidence_quote":"General-purpose synthesis and minimization baseline that the tool is compared against and combined with."},{"cited_title":"S.; and Yaroslavtsev, G","cited_arxiv_id":null,"evidence_quote":"Gives the $4.5n+o(n)$ upper bound for SUM in XAIG, the target the tool's SUM generators aim at."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Shows how to convert circuits to CNF, the standard step used for satisfiability checking and SAT-based synthesis."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"SAT solver interface used by the tool's satisfiability and synthesis routines."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the classification approach that lets the database cover all 3-input, 3-output functions through representatives."},{"cited_title":"J.; and Blott, M","cited_arxiv_id":null,"evidence_quote":"Source of the 32 neuron benchmarks from the contest that the tool optimized."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"QBF-based exact synthesis tool used alongside Cirbo on neuron benchmarks."}],"review_version":1}