Investigation of observability property of controlled binary
dynamical systems: a logical approach
G A Oparin, V G Bogdanova and A A Pashinin
Matrosov Institute for System Dynamics and Control Theory of SB RAS, Lermontov
St. 134, Irkutsk, Russia, 664033
bvg@icc.ru
Abstract. The property of observability of controlled binary dynamical systems is investigated.
A formal definition of the property is given in the language of applied logic of predicates with
bounded quantifiers of existence and universality. A Boolean model of the property is built in
the form of a quantified Boolean formula accordingly to the Boolean constraints method
developed by the authors. This formula satisfies both the logical specification of the property
and the equations of the binary system dynamics. Aspects of the proposed approach
implementation for the study of the observability property are considered. The technology of
checking the feasibility of the property using an applied microservice package is demonstrated
in several examples.
1. Introduction
Binary dynamical systems (BDS) are widely used in bioinformatics [1, 2], cryptography [3, 4], the
study of fault tolerance of computer networks [5, 6], and in many other subjects areas. Recently, the
BDS study has attracted considerable attention in systems biology. In particular, it is used as a model
of genetic regulatory networks [7]. In our research [8], the Boolean constraints method for the
qualitative analysis of BDS dynamic properties is proposed. This method is based on the following
provisions:
1. Formalization of dynamic properties definitions in the language of predicate logic and the use
of bounded quantifiers of existence and universality;
2. Conversion of the logical property formula that includes the equations of the BDS dynamics;
3. Elimination of bounded quantifiers and obtaining a property formula in the applied logic of
predicates with unbounded quantifiers.
A model of the dynamic property in the form of a Boolean constraint is obtained using the
sequential execution of these three stages. This model has the form of a Boolean equation or
quantified Boolean formula (QBF). The verification of the BDS property is reduced to the Boolean
satisfiability problem or verifying QBF truth. These problems are solved using modern SAT [9] and
QSAT [10] solvers. In recent years, there has been a significant increase in the performance of
specialized algorithms for solving SAT and QSAT problems due to using effective heuristics and deep
parallelization of the computational process. Therefore, the variables number in the dynamic property
model can be thousands.
_____________
Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0
International (CC BY 4.0).
The Boolean constraint method is a fairly general method for the qualitative analysis of BDS on a
finite time interval. In [8], this method is used for qualitative analysis of autonomous systems. This
study aims to use this method for a qualitative analysis of the observability property of controlled
BDS.
The article is structured as follows. Section 2 provides a brief overview of the use of dynamic
models in solving the observability problem. In Section 3, a mathematical model of a controlled BDS
and a problem statement for verifying k-observability for this model are presented. In Section 4, a
Boolean equation equivalent to the original system and a formal definition of k-observability is given.
Also, a Boolean model of this property in the form of a quantified Boolean formula is obtained. The
tools and model transformations used for the computer solution of the k-observability problem are
indicated in Section 5. In Section 6, the proposed technology of qualitative analysis of the k-
observability property for controlled BDS is demonstrated in several examples. The final Section 7
offers the advantages of the proposed method.
2. Related work
Observability is one of the fundamental notions in general control theory [11]. In particular, this
applies to the BDS control theory. Observability in control theory is a property that determines the
possibility of unambiguous recovery of information about the states of a system from a known output
on a finite time interval.
In the last decade, many publications have been devoted to the observability property of BDS
(Boolean networks). In [7, 12, 13, 14, 15], various definitions and methods for verifying this property
have been proposed. In [12-15], the study of the observability property is based on the approach using
the semi-tensor product (STP) of matrices [16]. As noted in [12], such an approach has a disadvantage
since the dimension of the obtained matrix is 2 n 2 n . This disadvantage is the computation
complexity for a high dimension n of the BDS state vector. In [13], an estimate of the acceptable value
of the dimension n (n <25) is given. For testing observability, an approach based on the idea of
representing BDS in polynomial form was proposed [7]. As the authors noted, computing a Gröbner
basis [17] used in this method leads, in the general case, to double exponential complexity. In
particular, for loosely coupled genetic regulatory networks, the method proposed in [7] is applicable
for significantly larger dimensions of the state vector of their Boolean models comparing with the STP
method.
A comparative analysis of different types of observability is presented in [18]. Checking the
observability property has high computational complexity. So the problem of reducing and speeding
up enumeration is fundamental for all the proposed methods. Based on the authors’ Boolean
constraints method, this problem is solved by SAT [9] and QSAT [10] solvers efficiently.
3. Problem statement
A nonlinear BDS of the following form is considered:
x t 1 F ( x t , u t ), y t H ( x t ), (1)
where x(t ) B n is the state vector, B {0,1} , u (t ) B m is the input (control) vector, y B l is the
output vector, n, m, l are dimensions of state, control, and output vectors, respectively;
t T {0,1,2,..., k 1} is the discrete time; F (x, u), H(x) are vector functions of logic algebra, called,
respectively, the transition and output function ( F : B n B m B n , H : B n B l ) .
The value k in the definition of the set T is assumed to be a predetermined constant. This limitation
occurs for the following reason. In a qualitative study of the behavior of the trajectories of system (1),
of practical interest is the feasibility of some dynamic property for a fixed, not too large k.
For each state x 0 B n called initial state and for any finite sequence of control vector states
u * [u 0 , u 1 ,...,u k 1 ] , let us define for the system (1) a trajectory x(t , x 0 , u * ) and an output function
y(t , x 0 , u * ) as finite sequences of states [ x 0 , x1 ,..., x k ] and y * [ y 0 , y1 ,..., y k 1 ] from sets B n and B l
respectively. In what follows, the sequence [ x1 ,..., x k ] will be denoted by x * .
It is necessary to check for system (1) the satisfiability of the k-observability property. We use the
following definition of this property, one of several definitions given in [19]. For any two different
states x0 , ~
x0 , there is an input sequence u * of length k such that the corresponding output sequences do
not coincide ( y * ~ y * ).
4. Solution method
For k 1 (only one-step transitions are considered), system (1) with an initial state x 0 and input
action u * [u 0 ] is equivalent to one Boolean equation of the following form:
L( x 0 , x1 , u 0 , y 0 ) ( x F ( x , u )) ( y H ( x )) 0 ,
n
i 1
1
i i
0 0 l
i 1
0
i i
0
where xit , y it (t = 0, 1) are i-th components of vectors x t , y t ; Fi , H i are i-th components of
vector-functions F and H; is the addition modulo-2 operation.
For multistep transitions ( k 1 ), system (1) is correspondingly equivalent to the following
Boolean equation:
( x 0 , x * , u * , y * ) k 1 t
t 0 L( x , x
t 1
,ut , yt ) 0 . (2)
For the initial state ~
x 0 , equation (2) takes the form
x , x , u , y ) tk01 L( ~
~ 0 ~* * ~*
( ~ x t 1 , u t , ~
xt,~ yt ) 0. (3)
According to the method of Boolean constraints, we write the formal definition of the k-
observability of a BDS in the language of applied logic of predicates with bounded quantifiers:
(x 0 , ~
x 0 : x0 ~
x 0 )(u * )(t T ) y(t , x 0 , u * ) y(t , ~
x 0 , u* ) .
Let us get rid of the bounded quantifiers of existence and universality and bear in mind the
equations of the dynamics of the BDS (2, 3) for various initial conditions. We obtain the following
Boolean model of the observability property in the form of a quantified Boolean formula:
(x 0 , ~
x 0 )(x * , ~
x * , u* , y* , ~
y * )(E ( x 0 , ~
x 0 ) ( x 0 , x * , u * , y * )
, (4)
~ 0 ~* * ~*
( ~x , x , u , y ) ( k 1 E ( y t , ~ y t )))
t 0
where the function E with appropriate arguments satisfies the following Boolean constraint:
E( z1 , z 2 ) (z z z z ) 0 .
p
i 1
1
i i
2 1
i
2
i
This constraint is equivalent to the condition of equality of two Boolean vectors z 1 and z 2 of the
dimension p. The total number of subject variables in formula (4) is 2k (n m l ) 2n .
5. Some aspects of program implementation
The implementation of the proposed approach to the qualitative analysis of the considered dynamic
property is based on the Boolean constraints method and performed in the form of an applied
microservices package (AMP) [20]. This AMP was created based on the HPCSOMAS framework
[21].
The AMP provides the following tools for automating the solving problems of qualitative analysis
and structural-parametric synthesis of BDS (Figure 1):
Constructing Boolean models of the dynamic properties of autonomous and controlled BDS;
Solving a separate problem of the qualitative analysis of BDS (checking the feasibility of a
dynamic property);
Solving complex problems of qualitative analysis of BDS, including performing several
separate tasks with alternating construction of Boolean models and checking their feasibility;
Graphic and tabular visualizing of obtained results.
The listed facilities are structured as separate complexes (processors) of the package. Access to the
complexes is performed through the user Dew agent [22]. In figure 1, the structural connections of
AMP complexes, grouped in these complexes objects and corresponding used layers of knowledge are
shown. The conceptual model of AMP, the construction and use of AMP for solving the problems of
qualitative analysis of BDS are discussed in detail in [20].
Figure 1. AMP structure.
For checking the observability property, complexes for constructing Boolean models and
qualitative analysis of controlled BDS are used. For conversing Boolean expressions in dynamic
properties models to CNF, the Tseitin transform [23], the Plaisted-Greenbaum transform [24], and the
transformation of the Boolean equation ANF = 0 to the form CNF = 1 [25] are used.
For solving Boolean satisfiability problems or checking the QBF truth, computational
microservices are used. These microservices are implemented based on the AllSAT solver
nbc_minisat_all-1.0.2 [26] and the QSAT solver DepQBF [27]. In the case of a high dimension of the
BDS state vector, previously developed parallel solvers [28, 29] of a similar purpose are used.
6. Illustrative example
The first example shows a detailed computation process.
6.1. Example 1
Let us consider the following controlled BDS (n=3, m=1, l=1):
x1t 1 x 2t x3t x 2t x3t
x 2t 1 x1t u t x1t u t
. (5)
x3t 1 x 2t
y t x1t x 2t x3t x1t x 2t x3t x1t x 2t x3t x1t x 2t x3t
System (5) is equivalent to the following one-step transition equation:
L( x10 , x20 , x30 , x11 , x12 , x31 , u 0 , y 0 ) x11 x20 x30 x11 x20 x30 x11 x20 x30 x11 x20 x30
x12 x10 u 0 x21 x10 u 0 x21 x10 u 0 x12 x10 u 0 x31 x20 x31 x20
.
x10 x20 x30 y 0 x10 x20 x30 y 0 x10 x20 x30 y 0 x10 x20 x30 y 0
x10 x20 x30 y 0 x10 x20 x30 y 0 x10 x20 x30 y 0 x10 x20 x30 y 0 0
To check the property of 3-observability, we write down the Boolean equation of a two-step
transition for the initial state x10 , x 20 , x30 :
( x10 , x 20 , x30 , x11 , x12 , x31 , x12 , x 22 , x32 , u 0 , u 1 , y 0 , y 1 )
.
L( x10 , x 20 , x30 , x11 , x12 , x31 , u 0 , y 0 ) L( x11 , x12 , x31 , x12 , x 22 , x32 , u 1 , y 1 ) 0
~
The Boolean equation 0 for a two-step transition with the initial state ~ x10 , ~
x20 , ~
x30 is written
similarly. In total, expression (4) contains 26 subject variables and 82 clauses. Boolean encoding of
subject variables is given in Table 1.
Table 1. Boolean encoding.
Variable x10 x 20 x30 u0 y0 x11 x12 x31 u1 y1 x12 x 22 x32
Code 1 2 3 4 5 6 7 8 9 10 11 12 13
Variable ~
x01
~
x02
~
x03 u~ 0 ~
y0 ~
x11
~
x12
~
x13 u~ 1 ~y 1 ~
x21
~
x22
~
x2
3
Code 14 15 16 17 18 19 20 21 22 23 24 25 26
When generating Boolean constraints by expression (4), the Plaisted-Greenbaum transform is used.
When applying this transformation, two additional variables are introduced. These variables are coded
as 27 and 28.
The expression (4) in QDIMACS format is given in Figure 2.
Figure 2. QBF for verifying observability property for system (5).
The QBFTV (QBF True Verification) service developed based on the QSAT-solver DepQBF for
the quantified Boolean formula (4) returns a message that this formula is TRUE, which means the
feasibility of the 3-observability property for system (5). The QBFTV service interface is shown in
Figure 3. The QBF in QDIMACS format is used as the input file. The execution result can be viewed
on the "Results" tab.
6.2. Example 2
Let us consider the Boolean model of the controlled system from [19] (n=10, m=3, l=7):
x1t 1 x 3t x 7t x8t x8t 1 x3t x 4t x9t
x 2t 1 x1t x9t 1 x5t x10
t
x 3t 1 x 4t x 9t t 1
x10 u1t (u 2t u 3t x 6t )
x 4t 1 x 2t x 5t y it xit , i 1,2,6,7 (6)
x 5t 1 u1t u 2t x 6t y 3t x3t x8t
x 6t 1 x1t y 4t x 4t x9t
x 7t 1 u1t y 5t x5t x10
t
Figure 3. QBFTV service interface.
The one-step transition equation for system (6) has the following form:
L( x10 , x 20 ,..., x10
0
, x11 , x12 ,..., x10
1
, u10 , u 20 , u 30 , y10 , y 20 ,..., y 70 ) x11 x30 x70 x80 x11 x30 x11 x70 x11
x80 x 21 x30 x12 x30 x31 x 40 x90 x31 x 40 x31 x90 x 41 x 20 x50 x14 x 20 x14 x50
x51 u10 u 20 x60 x51 u10 x51 u 20 x51 x60 x61 x10 x16 x10 x71 u10 x17 u10 x81
x30 x81 x 40 x90 x81 x30 x 40 x81 x30 x90 x91 x50 x10
0
x91 x50 x91 x10
0
x10
1
u10
u 20 x10
1
u10 u 30 x60 x10
1
u10 x10
1
u 20 u 30 x10
1
u 20 x60 y10 x10 y10 x10 y 20 x 20
y 20 x 20 y 30 x30 x80 y 30 x30 y 30 x80 y 40 x 40 y 40 x90 y 40 x 40 x90 y 50 x50 x10
0
y 50 x50 y 50 x10
0
y 60 x60 y 60 x60 y 70 x70 y 70 x70 0
To check the property of 3-observability, we write down the Boolean equation of a two-step
transition ( k 2 ) for the initial state x10 , x20 ,..., x10
0
:
( x10 , x 20 ,..., x10
0
, x11 , x12 ,..., x10
1
, x12 , x 22 ,..., x10
2
, u10 , u 20 , u 30 , u11 , u 12 , u 31 , y10 , y 20 ,..., y 70 , y11 , y 12 ,..., y 17 )
k 1 t t t 1 t 1 t 1
t 0 L( x1 , x 2 ,..., x10 , x1 , x 2 ,..., x10 , u1 , u 2 , u 3 , y1 , y 2 ,..., y 7 ) 0
t t t t t t t
~
The Boolean equation 0 for a two-step transition with the initial state ~ x10 , ~
x20 ,..., ~
x100 is written
similarly. In total, expression (4) contains 100 subject variables and 230 clauses.
The QBFTV service for the quantified Boolean formula (4) gives a message that this formula is
FALSE, which means that the observability property for system (6) is not satisfied.
6.3. Example 3
Let us consider the Boolean model of the controlled system from [7] (n=37, m=3, l=4):
x11 x90 x18
0 1
x15 x34
0
x37
0
x 129 x12
0
x30
0
x 12 x14
0 1
x16 x13
0 1
x30 x 70 x 25
0
x31 x 20 1
x17 x33
0 1
x31 x 20
0
x 14 x37
0 1
x18 x17
0 1
x32 x80
x51 x 60 1
x19 x37
0 1
x33 x 25
0
x 16 x32
0
x120 x 24
0
u10 u 20 1
x34 x11
0
x 17 x 26
0
x121 x 28
0 1
x35 x 40 u 30 (7)
x81 x 21
0
x122 x30 1
x36 x10
0
( x 20
0
x 27
0
)
x91 x80 x123 x16
0 1
x37 x 40 x 20
0
x36
0
1
x10 x 20
0
u 20 x35
0
u 20 x124 x10
0
x35
0
y10 x10
1
x11 x19
0
x125 x 70 y 20 x50
1
x12 x19
0
x126 x 27
0
x34
0
x37
0
( x15
0
x31
0
) y 30 x 22
0
1
x13 x 25
0
x127 x19
0
y 40 x 23
0
1
x14 x 26
0
x128 x 29
0
The one-step transition equation for system (7) has the following form:
L( x10 , x 20 ,..., x37
0
, x11 , x 12 ,..., x37
1
, u10 , u 20 , u 30 , y10 , y 20 , y 30 , y 40 ) x11 x90 x18
0
x11 x90 x11 x18
0
x 21
x14
0
x 12 x14
0
x31 x 20 x31 x 20 x 41 x37
0
x 14 x37
0
x51 x 60 x51 x 60 x 61 x32
0
x 16
x32
0
x 71 x 26
0
x 17 x 26
0
x81 x 21
0
x81 x 21
0
x91 x80 x91 x80 x10
1
x 20
0
u 20 x10
1
x35
0
u 20 x10
1
x 20
0
x35
0
x10
1
x35
0
u 20 x10
1
x 20
0
u 20 x10
1
u 20 x11
1
x19
0
x11
1
x19
0
x12
1
x19
0
x12
1
x19
0
x13
1
x 25
0
x13
1
x 26
0
x14
1
x 27
0
x14
1
x 27
0
x15
1
x34
0
x37
0
x15
1
x34
0
x15
1
x37
0
x16
1
x13
0
x16
1
x13
0
x17
1
x33
0
x17
1
x33
0
x18
1
x17
0
x18
1
x17
0
x19
1
x37
0
x19
1
x37
0
x 20
1
x 24
0
u10 u 20 x 120 x 24
0
x 120 u10 x 120 u 20 x 21
1
x 28
0
x 121 x 28
0
x 22
1
x30 x 122
x30 x 23
1
x16
0
x 123 x16
0
x 24
1
x10
0
x35
0
x 124 x10
0
x 124 x35
0
x 25
1
x 70 x 125 x 70 x 26
1
x 27
0
x34
0
x37
0
x15
0
x 27
0
x34
0
x37
0
x31
0
x 126 x 27
0
x 126 x34
0
x 126 x37
0
x 126 x34
0
x 126
x15
0
x31
0
x 27
1
x19
0
x 127 x19
0
x 28
1
x 29
0
x 128 x 29
0
x 29
1
x12
0
x 29
1
x30
0
x 129 x12
0
x30
0
x30
1
x 70 x30
1
x 25
0
x30
1
x 70 x 25
0
x31
1
x 20
0
x31
1
x 20
0
x32
1
x80 x32
1
x80 x33
1
x 25
0
x33
1
x 25
0
x34
1
x11
0
x34
1
x11
0
x35
1
x 40 u 30 x35
1
x 40 x35
1
u 30 x36
1
x10
0
x36
1
x 20
0
x 27
0
x36
1
x10
0
x 20
0
x36
1
x10
0
x 27
0
x37
1
x 40 x 20
0
x36
0
x37
1
x 40 x37
1
x 20
0
x37
1
x36
0
y10 x10 y10 x10 y 20 x50 y 20 x50 y 30 x 22
0
y 30 x 22
0
y 40 x 23
0
y 40 x 23
0
0
To check the property of 3-observability, we write down the Boolean equation of a two-step
transition (k=2) for the initial state x10 , x20 ,..., x37
0
:
( x10 , x 20 ,..., x37
0
, x11 , x12 ,..., x37
1
, x12 , x22 ,..., x37
2
, u10 , u 20 , u 30 , u11 , u 12 , u 31 , y10 , y 20 , y30 , y 40 , y11 , y 12 , y31 , y 14 )
k 1 t t t 1 t 1 t 1
t 0 L( x1 , x 2 ,..., x37 , x1 , x 2 ,..., x37 , u1 , u 2 , u 3 , y1 , y 2 , y 3 , y 4 ) 0
t t t t t t t t
~
The Boolean equation 0 for a two-step transition with the initial state ~ x10 , ~
x20 ,..., ~ 0
x37 is written
similarly. In total, expression (4) contains 250 subject variables and 515 clauses. The QBFTV service
for the quantified Boolean formula (4) gives a message that this formula is FALSE, which means that
the observability property for system (7) is not satisfied.
7. Conclusion
The solution to the qualitative study problem of the k-observability property of nonlinear BDS on a
finite time interval is obtained using the authors' Boolean constraints method. Recently, BDS (Boolean
networks) have attracted considerable attention as computational models for genetic and cellular
networks. In this article, we consider observability as the feature determining the initial state of the
BDS for given input and output sequences of the length k unequivocally. Based on the logic
specification of the dynamic property of k-observability and the equations of dynamics of a binary
system, a feasibility condition for the k-observability property is obtained in the form of a quantified
Boolean formula. The verification of the truth of this formula can be performed using an efficient
QSAT solver. An advantage of the developed tools for checking the k-observability property is their
orientation to systems with a high dimension of the state, control, and output vectors and a long
interval of discrete-time variation. The proposed method implementation allows data parallelism. So
high scalability for increasing the number of variables in the Boolean constraint is provided.
Acknowledgments
The study was supported by the Ministry of Science and Higher Education of the Russian Federation,
project «Technologies for the development and analysis of subject-oriented intelligent group control
systems in non-deterministic distributed environments».
References
[1] Taou N S, Corne D W and Lones M A 2016 Evolving Boolean networks for biological control:
State space targeting in scale free Boolean networks IEEE Conference on Computational
Intelligence in Bioinformatics and Computational Biology (CIBCB) pp 1–6
[2] Helikar T, Kochi N, Konvalina J and Rogers J A 2011 Boolean Modeling of Biochemical
Networks The Open Bioinformatics Journal 5 16–25
[3] Zanin M and Pisarchik A N 2011 Boolean Networks for Cryptography and Secure
Communication Nonlinear Sci. Lett. B 1(1) 25–32
[4] Dubrova E and Teslenko M 2016 A SAT-Based algorithm for finding short cycles in shift
register based stream ciphers IACR Cryptology ePrint Archive p 1068
[5] Dubrova E, Teslenko M and Tenhunen H 2007 A computational model based on Random
Boolean Networks 2nd Bio-Inspired Models of Network, Information and Computing
Systems pp 24–31
[6] Dubrova E, Teslenko M and Tenhune H 2008 Self-Organization for Fault-Tolerance Self-
Organizing Systems. IWSOS vol 5343 ed K A Hummel and J P G Sterbenz (Berlin,
Heidelberg: Springer)
[7] Li R, Yang M and Chu T 2015 Controllability and observability of Boolean networks arising
from biology Chaos 25(2) 023104
[8] Oparin G, Bogdanova V and Pashinin A 2019 Qualitative analysis of autonomous synchronous
binary dynamic systems MESA 10(3) 407–419
[9] Gong W and Zhou X 2017 A survey of SAT solver AIP Conference Proceedings vol 1836 p
020059
[10] Marin P, Narizzano M, Pulina L, Tacchella A and Giunchiglia E 2016 Twelve years of QBF
evaluations: QSAT is PSPACE-hard and it show Fundam. Informaticae 149(1–2) pp 133–
158
[11] Terrell W J 1999 Some Fundamental Control Theory I: Controllability, Observability, and
Duality The American Mathematical Monthly 106(8) 705–719
[12] Cheng D and Qi H 2009 Controllability and observability of Boolean control networks
Automatica 45(7) 1659–1667
[13] Zhao Y, Qi H and Cheng D 2010 Input-state incidence matrix of Boolean control networks and
its applications Sys. Contr. Lett. 59(12) 767–774
[14] Fornasini E and Valcher M 2013 Observability, reconstructibility and state obververs of
Boolean control networks IEEE Trans. Aut. Contr. 58 1390–1401
[15] Laschov D, Margaliot M and Even G 2016 Observability of Boolean networks: A graph-
theoretic approach Automatica 49 2351–2362
[16] Cheng D 2007 Sime-tensor product of matrices and its applications. A survey Proc. 4th
International Congress of Chinese Mathematicians pp 641–668
[17] Bardet M, Faugère J-C and Salvy B 2015 On the complexity of the F5 Gröbner basis algorithm
Journal of Symbolic Computation 70 49–70
[18] Zhang K and Zhang L 2016 Observability of Boolean control networks: A unified approach
based on finite automata IEEE Trans. Aut. Contr. 61(9) 2733–2738
[19] Cheng D, Qi H, Liu T and Wang Y 2016 A note on observability of Boolean control networks
Sys. Contr. Lett. 87 76–82
[20] Oparin G A, Bogdanova V G and Pashinin A A 2020 Microservice approach to the qualitative
study of attractors of binary dynamic systems based on the Boolean constraint method
Proceedings of the 43rd International Convention on Information, Communication and
Electronic Technology (MIPRO), Opatija, 2020 pp 1904–1909
[21] Bychkov I V, Oparin G A, Bogdanova V G, Pashinin A A and Gorsky S A 2017 Automation
development framework of scalable scientific web applications based on subject domain
knowledge Parallel Computing Technologies. PaCT 2017 vol. 10421 ed V Malyshkin
(Cham: Springer, LNCS) pp 278–288
[22] Pashinin A and Bogdanova V 2020 Application of user dew agent in hybrid-computing
environments Proceedings of the 1st International Workshop on Advanced Information and
Computation Technologies and Systems (AICTS’20) (CEUR-WS Proceedings) 2858 pp 135–
145
[23] Tseytin G S 1983 On the complexity of derivation in propositional calculus Automation of
Reasoning. Symbolic Computation (Artificial Intelligence) ed J H Siekmann and G
Wrightson (Berlin, Heidelberg: Springer) pp 466–483
[24] Plaisted D A and Greenbaum S 1986 A Structure Preserving Clause Form Translation J.
Smbolic Computation 2(3) 293–304
[25] An ANF to CNF Converter using a Dense/Sparse Strategy. [Online]. Available:
https://doc.sagemath.org/html/en/reference/sat/sage/sat/converters/polybori.html.
[26] Toda T and Soh T 2016 Implementing efficient all solutions SAT solvers ACM Journal of
Experimental Algorithmics 21(1) 1–44
[27] Lonsing F and Biere A 2010 DepQBF: A dependency-aware QBF solver Journal of
Satisfiability, Boolean Modeling and Computation. 9 71–76
[28] Bogdanova V G, Gorsky S A and Pashinin A A 2020 HPC-based parallel software for solving
applied Boolean satisfiability problems in Proc. of the 43rd Int. Convention on Information
and Communication Technology, Electronics and Microelectronics (MIPRO), Opatija, 2020
pp 1006–1011
[29] Bogdanova V G and Gorsky S A 2019 Multiagent technology for parallel implementation of
Boolean constraint method for qualitative analysis of binary dynamic systems in Proceeding
of the 42nd International Convention on Information and Communication Technology,
Electronics and Microelectronics (MIPRO) Opatija, 2019 pp 1043–1048