Программа для оценивания эффективности декомпозиций трудных экземпляров задачи булевой выполнимости с применением произвольных решателей и возможностью варьирования их параметров
блэкбокс оптимизация проблема булевой выполнимости
Программа предназначена для построения оценок времени решения трудных примеров задачи булевой выполнимости (SAT). Она получает на вход SAT-задачу в DIMACS CNF формате, множество переменных по которому будет осуществляться её декомпозиция, произвольный SAT-решатель, набор его параметров и значения операционных параметров. Программа разбивает полученную на вход SAT-задачу на подзадачи путем означивания переменных из полученного на вход множества и оценивает среднее время решения подзадач с применением метода Монте-Карло. Результатом является оценка времени, требуемого для решения всей задачи. Фактически, программа реализует функцию вида "черный ящик", что позволяет использовать для её минимизации соответствующие алгоритмы.
Разработанная программа может применяться для решения трудных примеров задачи булевой выполнимости либо для оценки времени их решения при некоторой декомпозиции. Программа поддерживает широкий набор современных алгоритмов решения SAT, которые могут быть привлечены для решения конструируемых подзадач
Степан
Кочемазов
Евгеньевич
научный сотрудник
Отсутствует
Отсутствует
M-4029-2015
56335586300
561185
РОССИЯ
Игорь
Бычков
Вячеславович
директор
РОССИЯ
28.23.29
Программная реализация интеллектуальных систем
28.23.17
Логика в искусственном интеллекте
01.02.EP
COMPUTER SCIENCE, ARTIFICIAL INTELLIGENCE
Степан
Кочемазов
Евгеньевич
Разработка архитектуры и алгоритмов программы, реализация программного кода, тестирование
РОССИЯ
Олег
Заикин
Сергеевич
Постановка задачи, разработка структуры и алгоритмов работы программы, тестирование
РОССИЯ
РФФИ
ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ УЧРЕЖДЕНИЕ "РОССИЙСКИЙ ФОНД ФУНДАМЕНТАЛЬНЫХ ИССЛЕДОВАНИЙ"
1037739411489
Организация
Федеральное государственное бюджетное учреждение "Российский фонд фундаментальных исследований"
Федеральные государственные бюджетные учреждения
ИДСТУ СО РАН
Федеральное государственное бюджетное учреждение науки Институт динамики систем и теории управления имени В.М. Матросова Сибирского отделения Российской академии наук)
1023801757000
Организация
Министерство науки и высшего образования Российской Федерации
Федеральные государственные бюджетные учреждения