КОНСТРУКТИВНЫЙ ПОДХОД К ПРОВЕРКЕ ИСТИННОСТИ КВАНТИФИЦИРОВАННЫХ БУЛЕВЫХ ФОРМУЛ В РЕШАТЕЛЕ HPC0QALL

Высокая вычислительная сложность ряда задач анализа динамики и структурно -параметрического синтеза для разных классов динамических управляемых систем обусловливает разработку методов и средств их параллельного решения. На основе метода булевы х ограничений задачи качественного анализа поведения траектор ий двоичных динамических систем , функционирование которых рассматривается на конечном интервале времени, сводятся к решению задач булевой выполнимости и проверки истинности квантифицированных бул евых формул. Строится математическая модель исследуемого динамического свойства в виде системы булевых уравнений, учитывающая как спецификацию свойства, так и уравнения динамики конкретного объекта. Такой подход, в отличие от существующих, является деклара тивным и обеспечивает возможность параллелизма по данным. Для проверки истинности 2 -квантифицированных булевых формул разработан параллельный решатель Hpc2qall . В отличие от аналогичных решателей , Hpc2qall выдает не только результат проверки истинности фор мулы (SAT или UNSAT ), но и осуществляет конструктивное нахождение всех наборов значений переменных под квантором всеобщности, приводящих к результату UNSAT . Приводится пример применения конструктивного подхода для решения задач и синтеза стабилизирующей обр атной связи .