Работа посвящена задаче проверки логической эквивалентности булевых схем, сводимой к задаче выполнимости (SAT). Классические подходы на основе КНФ и CDCL-решателей теряют структурную информацию схемы, а существующие методы Cube-and-Conquer на базе And-Inverter графов (AIG) порождают гибридное представление «схема + КНФ-ограничения», несовместимое с индустриальными алгоритмами структурной минимизации. В данной работе предложен новый метод декомпозиции, при котором ограничения ветвления встраиваются непосредственно в топологию схемы в виде дополнительных выходов, а не вынесены во внешние дизъюнкты. Результатом каждого шага кубирования является чистый AIG, что позволяет применять мощные эвристики минимизации на каждом этапе рекурсии и существенно повысить эффективность верификации.

Васькин В.В. (науч. рук. Семёнов А.А.) Разработка преобразований, сохраняющих структуру булевых схем после подстановок значений функциональных вершин // Сборник тезисов докладов конгресса молодых ученых. Электронное издание. – СПб: Университет ИТМО, [2026]. URL: https://kmu.itmo.ru/digests/article/16888