Соревнования по синтезу булевых схем

Я расскажу про соревнования по логическому синтезу, которые проводятся в течение нескольких последних лет в рамках конференции International Workshop on Logic and Synthesis. Цель — синтезировать (за примерно полгода) как можно более эффективные схемы для данных булевых функций, заданных таблицами истинности. В 2023 году первое место в этом соревновании занял Google DeepMind, в 2024 — наша команда (JetBrains и Neapolis University Pafos), в 2025 — UC Berkeley и National Taiwan University. Команды использовали самые разные техники — машинное обучение, комбинаторная оптимизация, анализ булевых функций, SAT-солверы и другое. Я расскажу про некоторые из этих техник, а также про предстоящее соревнование.