Distributed model counting упирается в балансировку и кэш. Разбираем, как gDMC решает это через work-stealing и явный стек.
В задачах model counting (#SAT) система деградирует не из-за одной причины, а из-за сочетания факторов. Последовательные решатели упираются в пределы single-core: частоты не растут, а компонентный кэш требует всё больше памяти. Попытки масштабировать через distributed model counting часто переносят проблему выше по стеку. Статическая декомпозиция (cube-and-conquer) создаёт высокий initialization overhead и плохо справляется с неоднородными задачами. В итоге возникает классическая проблема straggler: общее время определяется самым медленным воркером, потому что нужно покрыть всё пространство решений, а не найти один ответ.
Альтернатива — динамическая балансировка через work-stealing. В gDMC это реализовано как solver-agnostic слой, который отделяет оркестрацию от логики решателя. Архитектура на C++ templates позволяет подключать существующие DPLL-style решатели почти без изменений. Это важный компромисс: вместо переписывания ядра (как в DMC) вводится обобщённый интерфейс с нулевой стоимостью абстракций на этапе выполнения. Цена — необходимость строго формализовать, какие состояния можно безопасно передавать между воркерами.
Ключевая идея реализации — отказ от неявного рекурсивного стека в пользу явной структуры (explicit stack). Это меняет модель исполнения. В обычном DFS подзадачи “зашиты” в call stack и не могут быть переданы. В gDMC каждая вершина содержит:
- локальные подзадачи,
- аккумулятор результата,
- ссылки на удалённые задачи,
- коэффициент масштабирования.
Такой стек становится одновременно планировщиком и точкой агрегации. Узел не может быть удалён, пока не вернутся результаты от “украденных” задач. Это напрямую влияет на latency: вместо блокировки воркер продолжает локальную работу, а синхронизация откладывается.
Work-stealing здесь ограничен верхней частью стека. Это не случайное упрощение, а защита от разрушения кэша. Component caching в #SAT чувствителен к контексту (особенно из-за clause learning). Если делиться произвольными подзадачами, можно получить неконсистентные результаты. gDMC вводит строгие условия: передавать можно только те узлы, чьи родительские зависимости уже “вынесены наружу”. Это снижает параллелизм, но сохраняет корректность.
Дополнительная сложность — взаимодействие с learned clauses. Они меняют пространство вывода, но не всегда логически следуют из локальной подзадачи. Это может “отравить” кэш (cache inconsistency). В распределённой системе проблема усиливается: воркер может не увидеть конфликт, который должен был очистить кэш. gDMC решает это через ограничение: шаринг допускается только для веток, где все компоненты проверены на выполнимость. Это добавляет overhead (SAT-проверки), но применяется редко и в верхних уровнях дерева, поэтому не становится узким местом.
С точки зрения orchestration используется master-worker модель с point-to-group стратегией. Мастер выбирает одного активного воркера как источник работы и перераспределяет задачи на несколько idle-нод. Это снижает сетевые накладные расходы и ускоряет “разогрев” кластера. Воркеры обмениваются не формулами, а компактными представлениями (частичные назначения и переменные компонента). Это уменьшает bandwidth и latency.
Практическая деталь — использование assumptions mode. Это позволяет сохранять внутреннее состояние решателя между задачами: variable activity, learned clauses, component cache. В отличие от систем, где каждая задача изолирована, здесь воркер накапливает знания. Это критично для throughput на сериях связанных подзадач.
По результатам экспериментов (бенчмарки соревнований) система показывает near-linear scalability и решает больше инстансов, чем DisCount и DMC. Точные метрики зависят от конфигурации, но тренд очевиден:
- меньше overhead на простых задачах (нет стадии разбиения,
- лучше балансировка на сложных (динамический stealing).
При этом есть осознанные компромиссы. Arbitrary-precision арифметика дороже, чем double в DMC. Ограничения на шаринг снижают максимальный параллелизм. Master остаётся точкой координации, хотя и не становится bottleneck в экспериментах.
В индустриальном контексте это выглядит как эволюционное улучшение архитектуры distributed solvers. Основной сдвиг — не в алгоритме подсчёта, а в управлении состоянием и границами задач. Такой подход хорошо ложится на современные кластеры, где стоимость коммуникации и дисбаланса часто выше, чем стоимость вычислений.
Источник информации
arXiv — крупнейший открытый репозиторий препринтов (с 1991 года, под эгидой Корнелла), где исследователи оперативно размещают рабочие версии статей; материалы общедоступны, но не проходят полное рецензирование, поэтому результаты следует считать предварительными и, по возможности, сверять с обновленными версиями или рецензируемыми журналами. arxiv.org