Параллельный решатель проверки истинности 2QBF формул Hpc2qall
двоичные динамические системы 2QBF Квантифицированные булевы формулы
Программа Hpc2qall предназначена для параллельного решения задач проверки истинности 2-квантифицированных булевых формул (2QBF) на вычислительных кластерах и ориентирована на применение при решении задач качественного анализа двоичных динамических систем, функционирование которых рассматривается на конечном интервале времени, на основе метода булевых ограничений. 
Программа Hpc2qall представляет собой масштабируемое MPI-приложение на языке C++. Главный процесс приложения организует динамическую очередь подзадач, получаемых в результате расщепления 2QBF формулы. В отличие от существующих 2QBF решателей, Hpc2qall выдает не только заключение об истинности 2QBF формулы, но и осуществляет конструктивное нахождение всех наборов переменных под квантором всеобщности, приводящих к заключению «FALSE". Приложение реализовано на основе метода полного поиска и использует параллелизм по данным.
Программа Hpc2qall предназначена для параллельного решения задач проверки истинности 2-квантифицированных булевых формул (2QBF) на вычислительных кластерах с SMP-узлами и ориентирована на применение при решении задач качественного анализа двоичных динамических систем, функционирование которых рассматривается на конечном интервале времени, на основе метода булевых ограничений. Согласно этому методу, математическая модель исследуемого динамического свойства учитывает как спецификацию свойства, так и уравнения динамики конкретного объекта, и строится в виде булева уравнения или булевой формулы с двумя кванторами, всеобщности и существования. Подкванторное выражение представлено в виде конъюнктивной нормальной формы.
Геннадий
Опарин
Анатольевич
Зам. директора по науке
Доктор технических наук
Профессор
A-6540-2016
6508315345
1498
РОССИЯ
Игорь
Бычков
Вячеславович
директор
РОССИЯ
20.53.17
Средства хранения информации
20.53.19
Средства обработки и поиска информации
20.15.05
Информационные службы, сети, системы в целом
02.02.AC
AUTOMATION & CONTROL SYSTEMS
02.02.ES
COMPUTER SCIENCE, HARDWARE & ARCHITECTURE
Сергей
Горский
Алексеевич
Постановка задачи, разработка архитектуры и алгоритмов программы, реализация программного кода, тестирование
РОССИЯ
Вера
Богданова
Геннадьевна
Постановка задачи, разработка математического и алгоритмического обеспечения.
РОССИЯ
РФФИ
ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ УЧРЕЖДЕНИЕ "РОССИЙСКИЙ ФОНД ФУНДАМЕНТАЛЬНЫХ ИССЛЕДОВАНИЙ"
1037739411489
Организация
Федеральное государственное бюджетное учреждение "Российский фонд фундаментальных исследований"
Федеральные государственные бюджетные учреждения
ИДСТУ СО РАН
Федеральное государственное бюджетное учреждение науки Институт динамики систем и теории управления имени В.М. Матросова Сибирского отделения Российской академии наук)
1023801757000
Организация
Министерство науки и высшего образования Российской Федерации
Федеральные государственные бюджетные учреждения