Программа для решения трудных экземпляров проблемы булевой выполнимости с применением метода опорных векторов
параметризация проблема булевой выполнимости машинное обучение
Программа предназначена для решения трудных экземпляров проблемы булевой выполнимости (SAT). По данной на вход исходной булевой формуле в формате КНФ на первом этапе с помощью CDCL-решателя решается семейство простых SAT-задач, полученных с помощью подстановки в исходную КНФ случайных значений некоторого числа случайно выбранных переменных (от 10 до 100). На втором этапе осуществляется обучение линейной SVM-машины на конфликтных дизъюнктах, которые сгенерировал CDCL-решатель на первом этапе. При этом конфликтный дизъюнкт считается полезным, если он не был удален к моменту нахождения решения хотя бы одной задачи из семейства. На третьем этапе на короткий промежуток времени запускается CDCL-решатель, после чего с помощью обученной SVM-машины оценивается полезность всех сгенерированных конфликтных дизъюнктов. На четвертом этапе к исходной КНФ добавляются дизъюнкты, полезность которых была определена на третьем этапе, после чего на полученной КНФ запускается CDCL-решатель.
Решение задач комбинаторики и верификации.
Александр
Стрекаловский
Сергеевич
заведующий отделом
Доктор физико-математических наук
Профессор
M-1324-2014
6602292517
4230
РОССИЯ
Игорь
Бычков
Вячеславович
директор
РОССИЯ
28.23.29
Программная реализация интеллектуальных систем
28.23.17
Логика в искусственном интеллекте
01.02.EP
COMPUTER SCIENCE, ARTIFICIAL INTELLIGENCE
Олег
Заикин
Сергеевич
Разработка структуры и алгоритмов работы программы, реализация программного кода
РОССИЯ
Степан
Кочемазов
Евгеньевич
Разработка алгоритмов, проверка корректности результатов
РОССИЯ
ФАНО России
Федеральное агентство научных организаций
5137746009462
Организация
Правительство Российской Федерации
Федеральные государственные бюджетные учреждения
ИДСТУ СО РАН
Федеральное государственное бюджетное учреждение науки Институт динамики систем и теории управления имени В.М. Матросова Сибирского отделения Российской академии наук)
1023801757000
Организация
Министерство науки и высшего образования Российской Федерации
Федеральные государственные бюджетные учреждения