Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis
Authors: Daniil Averkov, Tatiana Belova, Gregory Emdin, Mikhail Goncharov, Viktoriia Krivogornitsyna, Alexander S. Kulikov, Fedor Kurmazov, Daniil Levtsov, Georgie Levtsov, Vsevolod Vaskin, Aleksey Vorobiev
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | 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. ... 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%. ... Table 1: Circuit size for a selection of benchmarks from IWLS 2024 Programming Contest from various categories. |
| Researcher Affiliation | Collaboration | 1St. Petersburg State University 2Steklov Mathematical Institute at St. Petersburg, Russian Academy of Sciences 3ITMO University 4 Ecole Polytechnique F ed erale de Lausanne 5Neapolis University Pafos 6Jet Brains Research |
| Pseudocode | Yes | Listing 1: Analyzing Boolean functions. ... Listing 2: Checking whether a circuit is satisfiable. ... Listing 3: Verifying that two circuits compute the same function. ... Listing 4: Reducing the factorization problem to circuit satisfiability. ... Listing 5: Synthesizing a circuit for the majority function. ... Listing 6: Synthesizing Full Adder using SAT-based approach. ... Listing 7: Synthesizing a circuit for MAJ6 using a hybrid approach. ... Listing 8: Cleaning an XAIG circuit for MAJ7. ... Listing 9: Cleaning an AIG circuit for MAJ7 using ABC. ... Listing 10: SAT-based minimization of a circuit for SUM5. Figure 1: A circuit (known as Full Adder) and the corresponding straight line program (in Python) for SUM3. |
| Open Source Code | Yes | Code https://github.com/SPb SAT/cirbo ... the code is open source2 and written in Python ... 2The code is publicly available at https://github.com/SPb SAT/cirbo. |
| Open Datasets | Yes | The goal of the competition is to synthesize efficient circuits for 100 Boolean functions (specified by their truth tables), in two bases, XAIG and AIG. ... the datasets in 2024 contest were the same as in 2023 ... In the IWLS 2024 Programming Competition, there were many benchmarks whose structure was unclear: for example, 32 benchmarks correspond to three-output neurons from the Logic Nets project (Umuroglu et al. 2020). |
| Dataset Splits | No | The paper refers to "benchmarks" from the IWLS 2024 Programming Contest and functions from the "Logic Nets project (Umuroglu et al. 2020)", which are predefined datasets used as a whole. It does not specify any training/validation/test splits of these datasets. |
| Hardware Specification | No | The paper does not provide specific hardware details (e.g., GPU models, CPU types, memory amounts) used for running the experiments. |
| Software Dependencies | No | The paper mentions several software tools and modules such as 'pysat module (Ignatiev, Morgado, and Marques Silva 2018)', 'ABC (Brayton and Mishchenko 2010)', 'mockturtle (Soeken et al. 2018)', 'CLI (Kulikov, Pechenev, and Slezkin 2022)', and 'CIOPS (Reichl, Slivovsky, and Szeider 2023)'. However, it does not specify explicit version numbers for any of these dependencies. |
| Experiment Setup | No | The paper describes various synthesis and minimization strategies and provides code snippets for implementing them, but it does not specify concrete experimental setup details such as hyperparameter values, learning rates, batch sizes, or specific training configurations for any learning-based components. |