REVIEW 4 major objections 6 minor 20 references
Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis
T0 review · 4 major / 6 minor · reviewed 2026-08-11 · deepseek-v4-flash
Pith's one-line read An open-source tool for Boolean circuits cuts the size of the best-known circuits by 12% on average and up to 83%.
desk verdict 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. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
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.
What would settle it
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.
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (4)
- [Abstract and Experimental Evaluation, Table 1] 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.
- [Arithmetic Functions, DIV construction] 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.
- [Related Work and Experimental Evaluation] 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.
- [Introduction and Database section] 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.
minor comments (6)
- [Introduction] The phrase 'the focus of the this paper' contains a typo; it should read 'the focus of this paper.'
- [Table 1] 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.
- [Boolean Circuits] 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.
- [Minimization] 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.
- [Database of (Nearly) Optimal Circuits] 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.
- [Experimental Evaluation, MAJ and SORT] 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.
Circularity Check
No significant circularity: the headline reductions are evaluated against external IWLS-2023 contest baselines, not against the authors' own fitted parameters or definitions.
full rationale
The paper's central empirical claim is that Cirbo reduced the best IWLS-2023 circuits by 12% on average (up to 83% for individual benchmarks). This comparison is made against externally maintained IWLS 2023/2024 contest datasets and the best circuits submitted by other teams in 2023 (Tables 1, 4-6), so the result is not equivalent to an input of the method by construction. The self-citations that appear — Demenkov et al. 2010 for the 4.5n+o(n) SUM upper bound, and Kulikov, Pechenev, and Slezkin 2022 for SAT-based local improvement — are either published external results or independent exact-synthesis routines whose correctness does not presuppose the paper's benchmark conclusions; they are components and background, not fitted parameters renamed as predictions. The unproved 5(n-i) comparison-subtraction subcircuit claim is a correctness and evidence gap, not a circularity: it is a local construction that could be checked against the open-source code and does not define the DIV/MOD result in terms of itself. The omission of the full per-benchmark distribution behind the 12% average weakens verifiability but is a reporting limitation, not a reduction of the claim to its own inputs. Overall, no load-bearing step in the derivation chain makes the predictions true by definition or by self-citation, so the circularity score is 0.
Assumptions & free parameters
assumptions (5)
- standard math Any binary Boolean operation can be computed by XOR, AND, and NOT gates without changing circuit size up to a constant factor.
- standard math Circuit SAT can be reduced to CNF SAT via the Tseitin transformation.
- standard math NPN classification with output permutation preserves circuit size.
- domain assumption The database of circuits for functions with at most three inputs and three outputs is correct, and the majority are provably optimal.
- domain assumption The combined comparison and subtraction subcircuit of size 5(n-i) for division works as described.
Cite this review
Pith. "Pith review of Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis." pith.science (2026). https://pith.science/paper/ZFVRTAVT
@misc{pith2026241214933,
author = {Pith},
title = {Pith review of: Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis},
year = {2026},
howpublished = {\url{https://pith.science/paper/ZFVRTAVT}},
note = {Machine review of arXiv:2412.14933}
}
read the original abstract
We present an open-source tool for manipulating Boolean circuits. It implements efficient algorithms, both existing and novel, for a rich variety of frequently used circuit tasks such as satisfiability, synthesis, and minimization. We tested the tool on a wide range of practically relevant circuits (computing, in particular, symmetric and arithmetic functions) that have been optimized intensively by the community for the last three years. The tool helped us to win the IWLS 2024 Programming Contest. In 2023, it was Google DeepMind who took the first place in the competition. We were able to reduce the size of the best circuits from 2023 by 12\% on average, whereas for some individual circuits, our size reduction was as large as 83\%.
Figures
Reference graph
Works this paper leans on
-
[1]
, " * write output.state after.block = add.period write newline
ENTRY address archivePrefix author booktitle chapter edition editor eid eprint howpublished institution isbn journal key month note number organization pages publisher school series title type volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.a...
-
[2]
write newline
" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...
-
[3]
Biere, A.; Heljanko, K.; and Wieringa, S. 2011. AIGER 1.9 And Beyond. Technical report, FMV Reports Series, JKU Linz, Austria
work page 2011
-
[4]
Biere, A.; Heule, M.; van Maaren, H.; and Walsh, T., eds. 2021. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press
work page 2021
-
[5]
Brayton, R. K.; and Mishchenko, A. 2010. ABC: An Academic Industrial-Strength Verification Tool. In CAV , volume 6174 of Lecture Notes in Computer Science, 24--40. Springer
work page 2010
-
[6]
Demenkov, E.; Kojevnikov, A.; Kulikov, A. S.; and Yaroslavtsev, G. 2010. New upper bounds on the Boolean circuit complexity of symmetric functions. Inf. Process. Lett., 110(7): 264--267
work page 2010
-
[7]
Find, M. G.; Golovnev, A.; Hirsch, E. A.; and Kulikov, A. S. 2016. A Better-Than-3n Lower Bound for the Circuit Complexity of an Explicit Function. In FOCS , 89--98. IEEE Computer Society
work page 2016
-
[8]
Find, M. G.; Golovnev, A.; Hirsch, E. A.; and Kulikov, A. S. 2023. Improving 3N Circuit Complexity Lower Bounds. Comput. Complex., 32(2): 13
work page 2023
Show all 20 references
-
[9]
Haaswijk, W.; Testa, E.; Soeken, M.; and Micheli, G. D. 2017. Classifying Functions with Exact Synthesis. In ISMVL , 272--277. IEEE Computer Society
2017
-
[10]
Ignatiev, A.; Morgado, A.; and Marques - Silva, J. 2018. PySAT: A Python Toolkit for Prototyping with SAT Oracles. In SAT , volume 10929 of Lecture Notes in Computer Science, 428--437. Springer
2018
-
[11]
A.; and Ofman, Y
Karatsuba, A. A.; and Ofman, Y. 1963. Multiplication of many-digital numbers by automatic computers. Dokl. Akad. Nauk SSSR, 145(2): 293--294
1963
-
[12]
S.; and Yaroslavtsev, G
Kojevnikov, A.; Kulikov, A. S.; and Yaroslavtsev, G. 2009. Finding Efficient Circuits Using SAT-Solvers. In SAT , volume 5584 of Lecture Notes in Computer Science, 32--44. Springer
2009
-
[13]
S.; Pechenev, D.; and Slezkin, N
Kulikov, A. S.; Pechenev, D.; and Slezkin, N. 2022. SAT-Based Circuit Local Improvement. In MFCS , volume 241 of LIPIcs, 67:1--67:15. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik
2022
-
[14]
Li, J.; and Yang, T. 2022. 3.1n-o(n) circuit lower bounds for explicit functions. In STOC , 1180--1193. ACM
2022
-
[15]
Reichl, F.; Slivovsky, F.; and Szeider, S. 2023. Circuit Minimization with QBF-Based Exact Synthesis. In AAAI , 4087--4094. AAAI Press
2023
-
[16]
Santhanam, R. 2022. Why MCSP Is a More Important Problem Than SAT (Invited Talk). In FSTTCS , volume 250 of LIPIcs, 2:1--2:1. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik
2022
-
[17]
Sch \" o nhage, A.; and Strassen, V. 1971. Schnelle Multiplikation gro er Zahlen. Computing, 7(3-4): 281--292
1971
-
[18]
Soeken, M.; Riener, H.; Haaswijk, W.; and Micheli, G. D. 2018. The EPFL Logic Synthesis Libraries. CoRR, abs/1805.05121
2018 arXiv
-
[19]
Tseitin, G. 1968. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, 115–--125
1968
-
[20]
J.; and Blott, M
Umuroglu, Y.; Akhauri, Y.; Fraser, N. J.; and Blott, M. 2020. LogicNets: Co-Designed Neural Networks and Circuits for Extreme-Throughput Applications. In FPL , 291--297. IEEE
2020
Reviewed August 11, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.