HPC-based parallel software for solving applied Boolean satisfiability problems

Boolean satisfiability is one of the fundamental problems in mathematical logic and the theory of computation. Many practical problems can be formulated as problems of Boolean satisfiability (solving a system of Boolean equations). These include the tasks of cryptography, qualitative research of binary dynamic systems, logical programming, robot action planning, and many others. NP-complexity of the Boolean satisfiability problem actualizes the development of parallel software for solving it in a high-performance computing environment. We focus on the development of specialized parallel solvers for Boolean satisfiability problems oriented to the application in the qualitative study of binary dynamic systems based on the Boolean constraint method. The Boolean constraint method uses a formal definition of the dynamical property, presented in the language of predicate logic with limited existential and universal quantifiers. Based on this definition, a model of dynamical property is formed in the form of Boolean constraints by a series of sequential formal transformations. The developed parallel solvers provide a conclusion on the feasibility of Boolean constraints, interpret this conclusion accordingly the tested property, and find, unlike similar software tools, all sets of values of Boolean variables that lead to this conclusion. An example of applying the developed solver to constructing cycles of a given length of stream ciphers based on shift registers is considered. The results confirming the effectiveness and scalability of the developed software are presented.