Аннотация:
В докладе рассмотрены эвристические методы по определению бит выполняющего набора задачи выполнимости булевых формул. Три из них представляют собой модификации метода простой итерации, применённом к непрерывному функционалу, ассоциированному с SAT: сочетание метода простой итерации с генетическим алгоритмом, применение байесовского подхода к проецированию вещественных переменных в булевы, изменение порядка вычисления переменных в методе простой итерации. Четвёртый представляет собой построение системы линейных уравнений на основе структуры 3-КНФ с последующим решением методом Гаусса-Зейделя.
Также разработан гибридный алгоритм, объединяющий все 4 разработанных подхода. Проведены численные эксперименты, в результате которых для каждого бита выполняющего набора получены частоты совпадения с соответствующими компонентами точного решения (тестирование проводилось на экземплярах 3-КНФ, эквивалентных задаче факторизации целых чисел).
|
