Circuit-Aware SAT Solving: Guiding CDCL via Conditional Probabilities

--- title: КОНТЕКСТ И ПРОБЛЕМАТИКА --- ### message ## КОНТЕКСТ И ПРОБЛЕМАТИКА В области Электронного Дизайна Автоматизированным Инструментарием (Electronic Design Automation, EDA), проблема Circuit Satisfiability (CSAT) является ключевым элементом для проверки логического эквивалентности (Logical Equivalence Checking, LEC) и других критических задач верификации. Традиционный подход к решению CSAT заключается в преобразовании схем в формулу в Канънской Нормальной Форме (Conjunctive Normal Form, CNF), которая затем обрабатывается общими SAT-решателями, основанными на Conflict-Driven Clause Learning (CDCL). Однако, такое преобразование часто приводит к потере важной структурной и функциональной информации, которая могла бы повысить эффективность решения. Традиционные подходы игнорируют богатую информацию о зависимостях между элементами схем, что может приводить к неоптимальному выбору критических переменных и неэффективному управлению клаузами. Это особенно заметно на крупных и сложных реальных схемах, где традиционные методы могут стать неэффективными из-за высокого уровня комплексности. Таким образом, необходимо разработать методы, которые сохраняют и используют структурную информацию схем напрямую, чтобы повысить эффективность SAT-решателей. ## ПРЕДЛОЖЕННЫЙ МЕТОД Для решения этой проблемы, авторы представляют CASCAD, инновационный circuit-aware SAT-решатель, который использует Graph Neural Networks (GNNs) для вычисления условных вероятностей на уровне логических элементов схемы. CASCAD построен на основе GNNs, которые моделируют зависимости между входами и выходами логических гейтов, позволяя эффективно вычислить условные вероятности. Эти вероятности затем используются для динамического руководства двух ключевых компонентов CDCL: выбор фазы переменных (variable phase selection) и управление клаузами (clause management). Ключевым элементом CASCAD является интеграция условных вероятностей непосредственно в процесс CDCL. Это позволяет решателю более информированно выбирать переменные и управлять клаузами на основе структурной информации схемы. Кроме того, CASCAD включает в себя стратегию probability-guided clause filtering, которая позволяет фильтровать клаузы на основе их вероятностей, что еще больше повышает эффективность решателя. ## ЭКСПЕРИМЕНТАЛЬНЫЕ РЕЗУЛЬТАТЫ Авторы провели обширные эксперименты на реальных бенчмарках LEC для оценки эффективности CASCAD по сравнению со стандартными CNF-based SAT-решателями. Результаты показали, что CASCAD снижает время решения до 10 раз по сравнению со стандартными подходами. Более того, использование probability-guided clause filtering дополнительно уменьшает время решения на 23,5%. Эти результаты демонстрируют значительное улучшение эффективности CASCAD по сравнению с традиционными методами. ## ПРАКТИЧЕСКАЯ ЗНАЧИМОСТЬ Практическая значеность CASCAD очевидна в контексте EDA, где эффективность SAT-решателей имеет прямое влияние на время и стоимость проектирования и верификации схем. Метод позволяет уменьшить время решения на больших и сложных схемах, что может привести к значительным экономиям времени и ресурсов в процессе разработки. Кроме того, CASCAD может быть интегрирован в существующие EDA инструменты, повышая их эффективность и надежность. ## ВЫВОДЫ И ПЕРСПЕКТИВЫ В заключение, CASCAD представляет собой значительный шаг вперед в области SAT-решателей, демонстрируя преимущества использования структурной информации схем напрямую в процессе решения. Будущие исследования могут фокусироваться на дальнейшем улучшении GNN-based моделей и их интеграции с другими EDA инструментами для повышения общей эффективности процесса проектирования и верификации.