Author name cluster

Gregory Emdin

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

2 author rows

AAAI Conference 2025 Conference Paper

Cirbo: A New Tool for Boolean Circuit Analysis and Synthesis

Daniil Averkov
Tatiana Belova
Gregory Emdin
Mikhail Goncharov
Viktoriia Krivogornitsyna
Alexander S. Kulikov
Fedor Kurmazov
Daniil Levtsov

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%.

PDF Details DOI

MFCS Conference 2022 Conference Paper

CNF Encodings of Parity

Gregory Emdin
Alexander S. Kulikov
Ivan Mihajlin
Nikita Slezkin

The minimum number of clauses in a CNF representation of the parity function x₁ ⊕ x₂ ⊕ … ⊕ x_n is 2^{n-1}. One can obtain a more compact CNF encoding by using non-deterministic variables (also known as guess or auxiliary variables). In this paper, we prove the following lower bounds, that almost match known upper bounds, on the number m of clauses and the maximum width k of clauses: 1) if there are at most s auxiliary variables, then m ≥ Ω(2^{n/(s+1)}/n) and k ≥ n/(s+1); 2) the minimum number of clauses is at least 3n. We derive the first two bounds from the Satisfiability Coding Lemma due to Paturi, Pudlák, and Zane using a tight connection between CNF encodings and depth-3 circuits. In particular, we show that lower bounds on the size of a CNF encoding of a Boolean function imply depth-3 circuit lower bounds for this function.

Details