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

Анотація наукової статті з математики, автор наукової роботи - Опарін Геннадій Анатолійович, Богданова Віра Геннадіївна, Горський Сергій Олексійович


The high computational complexity of some problems in the analysis of dynamics and structural-parametric synthesis for different classes of dynamic controlled systems leads to the development of methods and software for their parallel solution. Based on the Boolean constraints method, problems of qualitative analysis of the trajectories behavior of binary dynamical systems, whose operation is considered on a finite time interval, are reduced to solving Boolean satisfiability problems and checking the validity of quantified Boolean formulas. A mathematical model of the studied dynamic property is constructed as a system of Boolean equations, taking into account both the property specification and the equations of the dynamics of a specific object. Such an approach is declarative and provides the possibility of data parallelism. For verifying the validity of the quantified Boolean formulas, a parallel solver Hpc2qall was implemented. Unlike similar solvers, Hpc2qall not only produces the answer (SAT or UNSAT) but finds all values ​​sets of universally quantified variables leading to this answer. An example is given of applying a constructive approach to solving the problem of the synthesis of stabilizing feedback.


Область наук:

  • Математика

  • Рік видавництва: 2019


    Журнал

    Інформаційні та математичні технології в науці та управлінні


    Наукова стаття на тему 'КОНСТРУКТИВНИЙ ПІДХІД ДО перевірки істинності квантифікувати Булевой ФОРМУЛ В вирішувачі HPC2QALL'

    Текст наукової роботи на тему «КОНСТРУКТИВНИЙ ПІДХІД ДО перевірки істинності квантифікувати Булевой ФОРМУЛ В вирішувачі HPC2QALL»

    ?Конструктивний підхід до перевірки істинності квантифікованій булевих формул в УДК 004.421 + 004.4'2 + 004.771

    КОНСТРУКТИВНИЙ ПІДХІД ДО перевірки істинності квантифікувати Булевой ФОРМУЛ В вирішувачі HPC2QALL

    Опарін Геннадій Анатолійович

    Д.т.н., проф., Заст. директора, e-mail: Ця електронна адреса захищена від спам-ботів. Вам потрібно увімкнути JavaScript, щоб побачити її. Богданова Віра Геннадіївна к.т.н., доцент, с.н.с., e-mail: Ця електронна адреса захищена від спам-ботів. Вам потрібно увімкнути JavaScript, щоб побачити її. Горський Сергій Олексійович

    К.т.н., н.с., e-mail: Ця електронна адреса захищена від спам-ботів. Вам потрібно увімкнути JavaScript, щоб побачити її. Інститут динаміки систем і теорії управління імені В.М. Матросова Сибірського відділення Російської академії наук (ІДСТУ СО РАН), 664033 м Іркутськ вул. Лермонтова, 134

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

    Ключові слова: двійкова динамічна система, булева модель, паралельний 2QBF вирішувач, якісний аналіз.

    Цитування: Опарін Г.А., Богданова В.Г., Горський С.А. Конструктивний підхід до перевірки істинності квантифікованій булевих формул вирішувача Hpc2qall // Інформаційні та математичні технології в науці та управлінні. 2019. № 3 (15). С. 91-101. DOI: 10.25729 / 24130133-2019-3-08

    Вступ. Висока обчислювальна складність ряду завдань аналізу динаміки і структурно-параметричного синтезу для різних класів динамічних керованих систем, зокрема, NP-складність завдань якісного дослідження довічних динамічних систем (ДДС) [14], синтезу керуючої послідовності в ДДС [4],

    параметричного синтезу стабілізуючою зворотного зв'язку для керованих динамічних систем [10], обумовлює розробку методів і засобів їх паралельного рішення. На основі методу булевих обмежень [3] завдання якісного аналізу поведінки траєкторій довічних динамічних систем (ДДС), функціонування яких розглядається на кінцевому інтервалі часу, зводяться до вирішення завдань булевої здійсненності або перевірки істинності кваліфікованих булевих формул. Будується математична модель досліджуваного динамічного властивості у вигляді системи булевих рівнянь, що враховує як специфікацію властивості, так і рівняння динаміки конкретного об'єкта [1, 6]. Такий підхід, на відміну від існуючих, є декларативним і забезпечує можливість паралелізму за даними при рішенні задач великої розмірності. Мета цього дослідження полягала в розробці паралельного решателя перевірки істинності 2-квантифікованій булевих формул (2QBF). У розробленому вирішувача Hpc2qall застосовується паралелізм за даними. Підзадачі, отримані шляхом розщеплення вихідної 2QBF, вирішуються паралельно як незалежні. На відміну від існуючих 2QBF решателей, Hpc2qall видає не тільки результат перевірки істинності 2QBF, а й здійснює конструктивну знаходження всіх наборів змінних під квантором загальності, що призводять до результату UNSAT (значення формули одно FALSE), для цього в якості базового решателя використовується вирішувач CADET [12 ]. Що видається цим вирішувачів доказ правильності отриманого ним результату (сертифіката [11]) в разі хибності 2QBF (результат UNSAT) являє собою окремий випадок сертифіката, а саме, означивание змінних під знаком верхнього квантора загальності. Сертифікати дуже затребувані для практичних застосувань QBF [5, 11]. У даній роботі наводиться приклад застосування Hpc2qall для конструктивного вирішення завдання синтезу зворотного стабілізуючою зв'язку в ДДС на основі методу булевих обмежень.

    1. Постановка завдання. Розглядається нелінійна двоичная динамічна система (ДДС), векторно-матричне рівняння якої має вигляд

    x '= F (х' ~ \ і '~ 1), (1)

    у '- ^ Щх'-1). (2)

    де х, і, у - вектори відповідно стану, управління і виходу (х ^ В ", і ті Вт, у е В \ В = {ОД}), п, т і / - відповідні розмірності цих векторів;? е 71 = {1,2, ..., А} -діскретное час (номер такту); Е (х, і), Н (х) - векторні функції алгебри логіки,

    звані відповідно функцією переходів і виходу (F: В "ХВТ -> В ", H: В" - "В1).

    Ставиться завдання синтезу нелінійного закону управління з виходу на увазі зворотної

    зв'язку

    і-1 = о (/ - 1), (3)

    забезпечує глобальну стійкість заданого стану замкнутої системи.

    Система (1-3) на кінцевому інтервалі часу Т називається глобально стійкою

    щодо стану х *, якщо для будь-якого їй "існує момент часу ЕГ

    / * 0 \ * * * такий, що, х) = х, для всіх, тобто стан х є рівноважним станом

    (X (t \ х °) = х *) л (x (t * +1, х °) = X *). (4)

    Для заданого к = к * стабілізуючу зворотний зв'язок (3) назвемо оптимальної за швидкодією, якщо замкнута система (1-4) є глобально стійкою по відношенню до стану х *, але для к = к * -1 задача синтезу зворотного зв'язку не має рішення.

    2. Метод рішення. Будемо шукати функції Ог (у) (1 = \, 2, ..., т) в алгебраїчній

    нормальній формі (АНФ)

    &Лу) = с'о ®С [луг ®с \ ​​лу2 © ... © с; лу1 Фс; +1 л ^ лу2 Ф

    5 \ /

    ® С'г + 2 ЛУ \ Луз © ••• Фс2'-1 л

    де с) - невизначені коефіцієнти, сге {0,1} (/ = 1,2, ..., і; у = 0,1, ..., 2 '-1). позначимо

    безліч таких коефіцієнтів через С.

    Зведемо задачу синтезу стабілізуючою зворотного зв'язку до вирішення завдання перевірки істинності 2QBF, використовуючи метод булевих обмежень. Система рівнянь (1-3) з

    зворотним зв'язком виду (4) на інтервалі часу Т = {1,2, ..., А:} еквівалентна одному булеву

    рівняння виду

    Q>(X, Y, U, C) = 0,

    (6)

    де х = {х °, х \ ..., хк), у = {у °, у \ ..., ук-1), і = {і \ і \ ..., ик-1).

    Запишемо специфікацію завдання синтезу зворотного зв'язку, що забезпечує глобальну стійкість стану х *, на мові формальної логіки:

    (3C) (Vx °) (3t: t g T) ((x (t \ x °) = x *) A (x (t * + l, x °) = x *)).

    З урахуванням (6) це вираз набуде вигляду:

    (3C) (VX, 7, і: Ф (Х, 7, U, C) (3t: t е T) ((x (t *,) = х *) a (x (t * +1, х ° ) = х *)), (7)

    де Ф (Х, У, 1Т) - характеристична функція динамічного процесу з початковим станом х0 і безліччю коефіцієнтів С щодо змінних з множин

    XX, і.

    З урахуванням того, що характеристична функція стану х * має вигляд х, лж2 л- "лжп (ХГ - це змінна xi без заперечення для х * - 1 і з запереченням для

    х * = 0, / '= 1,2, ..., і) і в силу кінцівки безлічі Г подформулу

    {31 Л ^ Г) ((х (7 *, х °) = х *) л (х (7 * +1, х °) = х *)) замінимо на еквівалентну їй формулу

    % .Я ftit А ~ f + l \

    Замінимо обмежений квантор загальності на звичайний квантор загальності. Тоді (7) набуде вигляду

    (ЗС) (УХ, 7,? /) (Ф (Х, 7,? /, С) v ^ л? = 1 (* / лх / + 1)). (8)

    Позбудемося імплікації у формулі (8). Тоді отримаємо еквівалентну (8) 2QBF:

    (ЗС) (УХ, 7,? /) (Ф (ХХВД v (v? U Лп1 = 1 <х; лх; +1))). (9)

    Якщо значення цієї формули одно TRUE, то існує хоча б одне означивание коефіцієнтів з безлічі C, що є вирішенням завдання синтезу стабілізуючою зворотного зв'язку. В силу подвійності, якщо (9) істинна, то формула

    (УС) (ЗХЛ? /) (Ф (Х, ВДС) Л (Л ^ v; = 1 (*; vx / + 1))) (ю)

    помилкова. Отже, значення FALSE, отримане під час перевірки істинності (10), говорить про існування рішення задачі синтезу стабілізуючою зворотного зв'язку. Перевага розв'язання оберненої задачі полягає в можливості автоматизації уявлення подкванторного вираження у вигляді кон'юнктівной нормальної форми (КНФ) за допомогою конвертора, що надається програмними засобами Sage Tutorial [13], якщо ліва частина рівняння (6) задана у вигляді АНФ. КНФ використовується в форматі QDIMACS, необхідному для QBF-решателей.

    3. Ілюстративний приклад. Застосуємо розглянутий підхід для генетичної регуляторної мережі з керуючими входами [9], рівняння опису динаміки якої мають вигляд:

    i + i i / t i \ Xj = Щ Л (х2 V х3),

    t + l t t t x2 = Щ Л u2 Л Xj ,

    xf1 = і [Л (і \ V (u [• Xj)),

    t _ t

    y 1 * 1> (11)

    y \ = xl

    і [-1 = c \ ®c \ Л ^ Г ®c \ A y1; 1 ®c \ Л ^ Г ЛУ'2 ~ \ u2l = c? © с2лy'-1 © c22лy2l © c32лy'-1 лy2l, = Cq © cf л jf1 © c \ A y''1 © C33 A y1'1 A y " .

    Система булевих рівнянь (11) у форматі АНФ має вигляд:

    ф [= Xj е х2-1 е Хз-1 ф х2-1 1 Л< 4 © < _1 л х2-1 © і [~ 1 л Хз "1 Ф і [~ 1 л х2-1 л Хз" 1 = 0,

    ф'2 = х2 © И21 Л х [~ х Ф 1 I-л і 2 4 лхГ 1 = 0,

    Ф; = Х3 © t-1 / Т \ i-1 I-1 і 2 Ші3 л Xj © і2 -1 I-л і3 -1 I-1 ДЧ i-1 I-1 Л Xj © Щ л і 2 © і [~ 1 л З "1 л XI" 1 ©

    Ф і i-1 I-1 2 -1 i-1 i-1 Л з Л Xj = 0,

    ФГ '= УГ © хГ1 = 0,

    Ф'Г 1 = УГ © х2ч = 0,

    ф: г [I-1 = Mj © Зі © з \ Л у [~ 1 © 4 а У? © з \ лу [~ 1 = 0,

    Ф'7 [i-1 = і 2 © с2 © с2 л У; '© с2 а У? ®c? АУ [-1 лу? - = 0,

    ФГ 1 = і'3 ~ 1 © Cq © cl Л у [~ 1 © с23 А У? ®c? л ^ Г л в1 -, - 1 = 0.

    Використовуючи конвертор [13], наведемо кожне рівняння до виду КНФ = 1. для

    t еТ = {1,2, ..., до, до +1} отримаємо Ф (Х, Y, U, С) = д ^ 1 Ф [лФ2 л • • • ЛФ (8-1. Підставивши це

    значення в (10), отримаємо 2QBF:

    (V c) (3 x, 7, u) л ™ ф [л? 2 л-л ф ^ а (л t h v г1)).

    Значення коефіцієнтів з безлічі C, при яких ця формула помилкова, є рішеннями задачі синтезу стабілізуючою зворотного зв'язку.

    Для пошуку рішень цього завдання розроблений паралельний 2QBF вирішувач Hpc2qall. На відміну від існуючих 2QBF решателей, Hpc2qall видає не тільки висновок про істинність формули (SAT або UNSUT), але і здійснює конструктивну знаходження всіх наборів змінних під квантором загальності, що призводять до висновку UNSAT (значення формули одно FALSE). Ці набори значень є означивания коефіцієнтів з безлічі C. У розглянутому прикладі для t? {1,2} знайдені наступні набори таких значень, які є рішенням задачі синтезу стабілізуючою зворотного зв'язку:

    (0 0 0 0 1 1 0 0 0 10 0), (0 0 0 0 1 1 0 0 1 0 1 1), (0 0 0 0 1 1 0 0 0 1 1 1), (0 0 0 0 1 1 0 0 1 0 0 0), яким відповідають такі закони управління по виходу у вигляді зворотного зв'язку

    і [= 0, і'2 = 1 © Х = у [У'

    де fx = 1 J2 = у [®у [® у [-У2 = у [^ у [, / ред = \ ®у [® у [| у [= у [v y [JA = у [.

    3. Паралельний вирішувач Hpc2qall. У вирішувача Hpc2qall використовується паралелізм за даними. Підзадачі формуються на основі розщеплення вихідної 2QBF.

    Нехай х = (х1, ..., хі) і у - (у1, ..., у ") - вектори булевих змінних розмірності

    відповідно пх і п. Вирішувач Hpc2qall орієнтований на перевірку істинності 2QBF виду 0, хух ... уп0,2х \ - х "(р (у,: х), де квантори е! V, 3 !, а подкванторное вираз

    (Р {у, х) - (р (уХт .., уп, Л ',, ...) представлено в кон'юнктивній нормальній формі (КНФ). Для визначення здійсненності формули 2QBF, в якій ^ є квантором загальності, а - квантором існування, використовується паралельний алгоритм, заснований на розщепленні заданої 2QBF розглянутого виду шляхом виведення змінної у з-під верхнього квантора загальності відповідно до наступних правил перетворення:

    (12)

    А [Уу1з ..., у _! , У, +! , УПУ ^ ... ХП ,? (У, Х) у = 0]

    Якщо користуватися цією формулою, то при великій глибині розщеплення виникають накладні витрати, пов'язані з підстановкою констант, поширенням обмежень, спрощенням і т.д. Тому застосовується наступне перетворення

    V.v, ..... v ....., у Зх ^ ... * <р (у, X) = [V ^, ..., yi + 1, ..., у Ех ,, ... ^ у, (<р (у, х) л

    (13)

    А (у,))] A [V ^, ..., у1 + 1, ..., УПУ Е ^, ... ^, у, (<р (у, х) л С-СІ, -))] Очевидно, що (12) і (13) еквівалентні в силу наступного:

    3yi (<p (y, x) Ayi) = (c} (y, x) y = iAr) V (0>(Y, x) y = "A0) = Hу, x) y? = L ,

    3y, (c (y, x) A)) = (cp (y, X) y = iA0) V (p (y, x) yi = 0 Al) = kу, x) y? = 0 .

    Використовує розглянутий алгоритм розщеплення 2QBF паралельний вирішувач Hpc2qall є модифікованою версією решателя Hpcqsat [1]. Вирішувач Hpc2qall також реалізований на основі архітектури "Master-Slave" як MPI-додаток на мові C ++. Головний процес виконує аналогічні функції з формування черги подзадач і управління роботою дочірніх процесів.

    Вирішувачі Hpcqsat і Hpc2qall мають наступні відмінності:

    1. У Hpc2qall в якості базового решателя для перевірки істинності підзадачі в дочірніх процесах запускається 2QBF-вирішувач Cadet [12], в Hpcqsat - DepQBF.

    2. У Hpcqsat дочірній процес передає головному процесу запит на підзадачі і результат вирішення підзадачі (SAT або UNSAT), а в Hpc2qall додатково до результату рішення передається сертифікат, що повертається базовим вирішувачів Cadet.

    3. У разі отримання відповіді UNSAT від базового решателя Hpcqsat знаходить один набір значень булевих змінних, який привів до такої відповіді (конструктивне рішення). Hpc2qall може знайти все такі набори (за замовчуванням, а також один або k наборів, якщо задано відповідне значення параметра пошуку).

    4. Hpcqsat використовує дерево розщеплення 2QBF для пошуку конструктивного рішення, а Hpc2qall використовує сертифікат, переданий разом з результатом базовим вирішувачів Cadet. Сертифікат в даному випадку є значення змінних верхнього квантора, при яких даний результат був отриманий. При отриманні для підзадачі відповіді UNSAT головний процес решателя Hpc2qall здійснює побудова відповідної гілки дерева розщеплення на глибину верхнього квантора (процедура SetSubtaskPath, рис. 1), і присвоює їй значення UNSAT. У процесі формування даної гілки з'являється безліч відгалужень, які можуть також містити шукані значення, вони будуть оброблятися аналогічно в процесі виконання завдання. Представлені на рис. 1 і рис. 2 блок-схеми описують роботу головного (Master) і робочих процесів (Slave).

    Мінлива Solve перемикає режим роботи головного процесу з розщеплення 2QBF (Solve = 0) на управління роботою дочірніх процесів при вирішенні подзадач (Solve = 1). Кількість подзадач в черзі підтримується відповідно до кількості вільних обчислювальних ресурсів. Мінлива Result.val служить для вибору обробки результату, отриманого в дочірньому процесі при запуску процедури SolveByCadet (рис. 2). Аналіз впливу завантаження дочірніх процесів (кількості підзадач, що відправляються у відповідь на запит дочірнього процесу Send (Request)) наведено в [7]. Процедура addToRequest регулює формування завдання для дочірніх процесів. На рис. 3 приведено прискорення, отримане при вирішенні задачі синтезу стабілізуючою зворотного зв'язку для k = 2 (нижня лінія) і тієї ж завдання більшої розмірності (при k = 3 - верхня лінія). Видно, що зі збільшенням розмірності задачі прискорення стає близьким до лінійного. На рис. 4 наведені

    результати вирішення низки близьких за характеристиками тестових завдань [8], що показують однаково високу ефективність (рис. 5). Експерименти проводилися на кластері «Академік В.М. Матросов »[2].

    Мал. 1. Робота головного процесу

    З старт)

    Send (Request); // Надсилаємо запит на завдання Recv (&Task); // Отримуємо завдання

    про

    7

    ? 6 5 4 3

    Про CL Про &

    2

    32 64 96 128 160 192 224 256 Процесорні ядра

    1! к = 3

    Мал. 2. Робота дочірнього процесу

    Мал. 3. Прискорення на розглянутому прикладі

    5- 123456789 10 11 12

    Тестові завдання, 64 12s 256

    -32 -64 -128 256

    Мал. 4. Наростання загальний час Рис. 5. Ефективність вирішення тестових

    виконання тестових завдань (в сек.) завдань для 64, 128 і 256 процесорних ядер

    Висновок. Запропоновано конструктивний підхід до вирішення завдання перевірки істинності 2QBF. Розроблено паралельний 2QBF вирішувач Hpc2qall, який, на відміну від існуючих, видаючи відповідь UNSAT, дозволяє отримати значення змінних під першим знаком квантора загальності, при яких формула приймає помилкове значення. З використанням Hpc2qall вирішена задача синтезу закону керування по виходу у вигляді зворотного зв'язку, що забезпечує глобальну стійкість заданого стану замкнутої системи. Проведено ряд обчислювальних експериментів, які підтвердили працездатність і ефективність решателя.

    Дослідження виконано за підтримки РФФД, проект № 18-07-00596.

    СПИСОК ЛІТЕРАТУРИ

    1. Богданова В.Г., Горський С.А. Паралельна реалізація логічного методу вирішення завдань якісного аналізу довічних динамічних систем // Інформаційні та математичні технології в науці та управлінні. 2018. №4 (12). С. 145-154. DOI: 10.25729 / 2413-0133-2018-4-15.

    2. Іркутський суперкомп'ютерний центр. Режим доступу: http://hpc.icc.ru/ (дата доступу 30.06.2019).

    3. Опарін Г.А., Богданова В.Г., Пашинін А.А. Метод булевих обмежень в якісному аналізі // Міжнародний журнал прикладних і фундаментальних досліджень. 2018. № 9. С. 19-29. DOI: 10.17513 / mjpfi. 12381.

    4. Akutsu T., Hayashida M., Tamura T. Algorithms for inference, analysis and control of Boolean networks // International Conference on Algebraic Biology, 2008. Pp. 1-15. DOI: https://doi.org/10.1007/978-3-540-85101-l_l.

    5. Becker B., Ehlers R., Lewis M., Marin P. ALLQBF Solving by Computational Learning. In: Chakraborty S., Mukund M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science. 2012. Vol. 7561. Pp. 370-384. Springer, Berlin, Heidelberg. DOI: https://doi.org/10.1007/978-3-642-33386-6_29.

    6. Bogdanova V.G., Gorsky S.A. Multiagent technology for parallel implementation of Boolean constraint method for qualitative analysis of binary dynamic systems // 42nd International

    Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO). Opatija. 2019. Pp. 1043-1048. DOI: 10.23919 / MIPR0.2019.8757154.

    7. Bogdanova V.G., Gorsky S.A. Scalable parallel solver of Boolean satisfiability problems // 41st International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO), Opatija, 2018. Pp. 0222-0227. DOI: 10.23919 / MIPR0.2018.8400042.

    8. Datasets of 2QBF. Режим доступу: http://www.qbflib.org/eval18.html (дата доступ: 30.06.2019)

    9. Li H., Wang Y. Output feedback stabilization control design for Boolean control networks // Automatica. 2013. Vol. 49 (12). Pp. 3641-3645. DOI: https: // doi .org / 10.1016 / j. automatica.2013.09.023.

    10. Nemirovskii A.A. Several NP-hard problems arising in robust stability analysis // Mathematics of Control, Signals, and Systems. 1993. Vol. 6. Pp. 99-105. DOI: https: // doi .org / 10.1007 / BF01211741.

    11. Niemetz A., Preiner M., Lonsing F., Seidl M., Biere A. Resolution-Based Certificate Extraction for QBF. In: Cimatti A., Sebastiani R. (eds) Theory and Applications of Satisfiability Testing - SAT 2012. Lecture Notes in Computer Science. 2012. Vol. 7317. Pp. 430-435. Springer, Berlin, Heidelberg. DOI: https://doi.org/10.1007/978-3-642-31612-8_33.

    12. Rabe M.N., Seshia S.A .: Incremental Determinization. In: Creignou N., Le Berre D. (eds) Theory and Applications of Satisfiability Testing - SAT 2016. Lecture Notes in Computer Science. 2016. Vol. 9710. Pp. 375-392. Springer, Cham. DOI: https://doi.org/10.1007/978-3-319-40970-2_23.

    13. Sage Tutorial in Russian. Режим доступу: http://doc.sagemath.org/pdf/ru/tutorial/ SageTutorial_ru.pdf (дата доступу 30.06.2019)

    14. Zhao Q. "A remark on" Scalar equations for synchronous Boolean networks with biological Applications "by C. Farrow, J. Heidel, J. Maloney, and J. Rogers," in IEEE Transactions on Neural Networks, 2005. Vol. 16 (6). Pp. 1715-1716. DOI: 10.1109 / TNN.2005.857944.

    UDK 004.421 + 004.4'2 + 004.771

    A CONSTRUCTIVE APPROACH TO THE CHECKING OF VALIDITY OF 2-QUANTIFIED BOOLEAN FORMULAS IN THE HPC2QALL SOLVER

    Gennady A. Oparin

    Doctor of technical science, professor, Deputy Director, e-mail: Ця електронна адреса захищена від спам-ботів. Вам потрібно увімкнути JavaScript, щоб побачити її.

    Vera G. Bogdanova PhD., Assistant professor, senior researcher, e-mail: Ця електронна адреса захищена від спам-ботів. Вам потрібно увімкнути JavaScript, щоб побачити її.

    Sergey A. Gorsky PhD., Researcher, e-mail: Ця електронна адреса захищена від спам-ботів. Вам потрібно увімкнути JavaScript, щоб побачити її. Matrosov Institute for System Dynamics and Control Theory Siberian Branch of the Russian Academy of Sciences 134, Lermontov Str., 664 033, Irkutsk, Russia

    Abstract. The high computational complexity of some problems in the analysis of dynamics and structural-parametric synthesis for different classes of dynamic controlled systems leads to the development of methods and software for their parallel solution. Based on the Boolean constraints method, problems of qualitative analysis of the trajectories behavior of binary dynamical systems, whose operation is considered on a finite time interval, are reduced to solving Boolean satisfiability problems and checking the validity of quantified Boolean formulas. A mathematical model of the studied dynamic property is constructed as a system of Boolean equations, taking into account both the property specification and the equations of the dynamics of a specific object. Such an approach is declarative and provides the possibility of data parallelism. For verifying the validity of the quantified Boolean formulas, a parallel solver Hpc2qall was implemented. Unlike similar solvers, Hpc2qall not only produces the answer (SAT or UNSAT) but finds all values ​​sets of universally quantified variables leading to this answer. An example is given of applying a constructive approach to solving the problem of the synthesis of stabilizing feedback.

    Keywords: binary dynamic system, Boolean model, parallel 2QBF solver, qualitative analysis.

    References

    1. Bogdanova V.G., Gorsky S.A. Parallelnaya realizatsiya logicheskogo metoda resheniya zadach kachestvennogo analiza dvoichnykh dinamicheskikh system [Parallel implementation of the logical method for solving the problems of binary dynamic systems qualitative analysis // Informatsionnyye i matematicheskiye tekhnologii v nauke i upravlenii = Information and mathematical technologies in science and management. 2018. №4 (12). C. 145-154. DOI: 10.25729 / 2413-0133-2018-4-15 (in Russian)

    2. Irkutskiy superkomp'yuternyy tsentr [Irkutsk Supercomputer Center of SB RAS]. Available at: http://hpc.icc.ru/ (accessed 30.06.2019) (in Russian)

    3. Oparin G.A., Bogdanova V.G., Pashinin A.A. Metod bulevykh ogranicheniy v kachestvennom analize dvoichnykh dinamicheskikh system [Boolean constraints method in qualitative analysis of binary dynamic systems] // Mezhdunarodnyy zhurnal prikladnykh i fundamentalnykh issledovaniy = International Journal of Applied and Basic Research. 2018. № 9. Pp. 19-29. DOI: 10.17513 / mjpfi.12381 (in Russian)

    4. Akutsu T., Hayashida M., Tamura T. Algorithms for inference, analysis and control of Boolean networks // International Conference on Algebraic Biology, 2008. Pp. 1-15. DOI: https://doi.org/10.1007/978-3-540-85101-l_l.

    5. Becker B., Ehlers R., Lewis M., Marin P. ALLQBF Solving by Computational Learning. In: Chakraborty S., Mukund M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science. 2012. Vol. 7561. Pp. 370-384. Springer, Berlin, Heidelberg. DOI: https://doi.org/10.1007/978-3-642-33386-6_29.

    6. Bogdanova V.G., Gorsky S.A. Multiagent technology for parallel implementation of Boolean constraint method for qualitative analysis of binary dynamic systems // 42nd International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO). Opatija. 2019. Pp. 1043-1048. DOI: 10.23919 / MIPR0.2019.8757154.

    7. Bogdanova V.G., Gorsky S.A. Scalable parallel solver of Boolean satisfiability problems // 41st International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO). Opatija. 2018. Pp. 0222-0227. DOI: 10.23919 / MIPR0.2018.8400042.

    8. Datasets of 2QBF. Available at: http://www.qbflib.org/eval18.html (accessed 30.06.2019)

    9. Li H., Wang Y. Output feedback stabilization control design for Boolean control networks // Automatica. 2013. Vol. 49 (12). Pp. 3641-3645. DOI: https: // doi .org / 10.1016 / j. automatica.2013.09.023.

    10. Nemirovskii A.A. Several NP-hard problems arising in robust stability analysis // Mathematics of Control, Signals, and Systems. 1993. Vol. 6. Pp. 99-105. DOI: https: // doi .org / 10.1007 / BF01211741.

    11. Niemetz A., Preiner M., Lonsing F., Seidl M., Biere A. Resolution-Based Certificate Extraction for QBF. In: Cimatti A., Sebastiani R. (eds) Theory and Applications of Satisfiability Testing -SAT 2012. Lecture Notes in Computer Science. 2012. Vol. 7317. Pp. 430-435. Springer, Berlin, Heidelberg. DOI: https://doi.org/10.1007/978-3-642-31612-8_33.

    12. Rabe M.N., Seshia S.A .: Incremental Determinization. In: Creignou N., Le Berre D. (eds) Theory and Applications of Satisfiability Testing - SAT 2016. Lecture Notes in Computer Science. 2016. Vol. 9710. Pp. 375-392. Springer, Cham. DOI: https://doi.org/10.1007/978-3-319-40970-2_23.

    13. Sage Tutorial in Russian. Режим доступу: http://doc.sagemath.org/pdf/ru/tutorial/ SageTutorial_ru.pdf (дата доступу 30.06.2019)

    14. Zhao Q. "A remark on" Scalar equations for synchronous Boolean networks with biological Applications "by C. Farrow, J. Heidel, J. Maloney, and J. Rogers," in IEEE Transactions on Neural Networks, 2005. Vol. 16 (6). Pp. 1715-1716. DOI: 10.1109 / TNN.2005.857944.


    Ключові слова: Двійкова ДИНАМІЧНА СИСТЕМА /Булевой МОДЕЛЬ /ПАРАЛЕЛЬНИЙ 2QBF вирішувачі /ЯКІСНИЙ АНАЛІЗ

    Завантажити оригінал статті:

    Завантажити