Краткое содержание

arXiv:2511.07737v1 Тип объявления: кросс Аннотация: Хотя ускоренные вычисления преобразовали многие области вычислительной техники, их влияние на логическое рассуждение, особенно применительно к проверке выполнимости булевых формул (Boolean Satisfiability — SAT), остаётся ограниченным. Современные решатели SAT в значительной степени полагаются на изначально последовательные алгоритмы поиска, управляемые конфликтами, которые предлагают мощные эвристики, однако ограничивают степень параллелизма, который мог бы существенно повысить масштабируемость решения SAT-задач. Вдохновлённые тренировкой нейронных сетей, мы формулируем проблему SAT как слой бинаризированного матрично-матричного умножения, оптимизируемый с помощью дифференцируемой целевой функции. Благодаря этому представлению мы объединяем преимущества параллельной дифференцируемой оптимизации и последовательного поиска для ускорения SAT-решения на гибридной системе GPU–CPU. В этой системе графические процессоры используют параллельную дифференцируемую обработку для быстрого оценивания SAT-клауз и применяют градиенты для стохастического исследования пространства решений и оптимизации присваиваний переменных. Перспективный