In this research, we consider the problems of searching for collisions in cryptographic hash functions from the MD family as variants of the Boolean Satisfiability problem (SAT). To construct the SAT encodings for MD4 and MD5 algorithms, we employ the Transalg system designed to automatically transform algorithmic descriptions of discrete functions to Boolean equations. For hash functions under consideration, the SAT encodings are much more compact than known analogues, because the several additional constraints based on the known differential attacks on these functions are used in these encodings. The solving time for the SAT instances, encoding the search for single block collisions for MD4, is on average less than 1 sec on an usual PC. To solve the SAT instances, encoding the search for two-block collisions for MD5, we employed parallel SAT solvers working on the computing cluster. As a result, we found a class of two-block collisions for MD5 with the first 10 zero bytes. We constructed several dozens of collisions of the proposed kind. Also, we considered the inversion problem for the MD4 hash function (the search for the preimage for a given hash value). To solve this problem, we developed a technique relying on the so called variables. Each switch variable is responsible for an additional constraint on several Boolean variables included in the SAT encoding. If a switch variable takes the value of Truth then the corresponding constraint becomes enabled and should be taken into account by the SAT solving algorithm. Otherwise this constraint remains inactive. The use of switch variables made it possible to find new additional constraints (similar to Dobbertin's constraints) and to improve the effectiveness of solving the inversion problem for 39-step MD4 by a hundredfold.

In this report, the results of computational analysis are presented for problems of searching fixed points and cycles of some discrete mappings, that are used to model the behaviour of systems with many interconnecting agents and are defined by random graphs generated according to known models (G np-graphs, the Watts — Strogatz model).

The article i s devoted to converting combinatorial problems into the problems of solving Boolean equations. Some theoretical results are presented as the basis of technology for propositional encoding of algorithms calculating discrete functions. Software system Transalg implementing the technology is described. Examples of using the Transalg for translating cryptoanalysis algorithms to SAT-problem are presented. The technics for translating 0-1-ILP optimization algorithms into SAT are considered too.

In the report, we present results of applying symbolic computation algorithms to solving discrete automata research problems (e.g. problems of analysis of discrete models of gene networks) and combinatorial optimization problems. In all cases, an original problem is translated into Boolean equations (and after this to SAT) and then is solved using SAT-solver. Optimization problems are solved in distributed computing environments with the help of the SAT-solver specially developed for this task.

A technology for translating different combinatorial problems to the tasks of finding solutions of logical (Boolean) equations is presented. Theoretical possibility of translations of that sort was shown by S. Cook in 1971. The report is expected to describe in detail Transalg the new translator of algorithms to the propositional logic. Unlike previous developments this translator allows obtaining propositional encodings for algorithms computing arbitrary everywhere defined Register Machine-computable discrete functions. Actually a program computing this function should be written in a special high level (C-like) language. Translator was used for obtaining propositional encodings of some encryption algorithms, algorithms describing functioning the gene networks of a certain class and for translating the problems from 0-1 ILP to SAT.