G-RRM направляет символические решатели с помощью рекуррентных моделей рассуждений для задач удовлетворения ограничений

Авторы предлагают G-RRM, нейро-символический подход, который интегрирует символьно-эквивариантные рекуррентные модели рассуждений (SE-RRM) с классическими символическими решателями для повышения эффективности поиска в задачах удовлетворения ограничений. SE-RRM действуют как нейронные решатели, генерирующие предложения решений для направления методов обратного перебора или SAT-решателей, таких как Glucose 4.1 и CaDiCaL 3.0.0.

• Эффективность G-RRM требует обширных комбинаторных пространств поиска и архитектур решателей, способных динамически перезаписывать ветвящиеся выборы.
• На судоку $9\times9$, где SE-RRM решают 91.1% случаев, ускорение обратного перебора составляет 33.3x, а Glucose 4.1 — 1.70x.
• Glucose 4.1 сохраняет ускорение 1.17x на идеальных подсказках для сеток $25\times25$.
• CaDiCaL 3.0.0 не показывает значительного ускорения, поскольку он всегда уважает введенные подсказки, а не перезаписывает их.

Эти результаты очерчивают конкретные режимы, в которых нейронное направление приводит к практическому ускорению по реальному времени для символических решателей.