Scientific goal of the project

The project is aimed to solve various combinatorial problems. There are many practically important problems for which the existence of effective (polynomial) algorithms of their solving has not been proven. Most of these problems are NP-hard. It means that under some reasonable (albeit unproven) assumptions, these problems can not be solved in polynomial time. However, many of their special cases arise in practical applications: various discrete optimization problems (for example, planning of production) and problems of verification of discrete devices (arising, for example, in designing of circuits and proving of program correctness). Therefore it is very important to have methods for their solving that don't have polynomial complexity, but are effective in practice. Such methods can cope with the numerous special cases of NP-hard problems of huge dimensions. One of the most simple in its basis, and therefore the most efficient in terms of software implementations is SAT approach. This approach is based on reducibility of the considered original problem to a SAT problem, that is the problem of satisfiability of conjunctive normal form (CNF). SAT problems admit a very natural form of parallelism, allowing use of a distributed computing environments (including Grid). Actually reducibility to SAT can be carried out effectively (in fact, it follows from the famous theorem of Cook-Levin).

Cryptanalysis provides very attractive class of problems for solving of which SAT approach can be used. It should be noted that we don't solve problems of deciphering some private data. All the tests under consideration are randomly generated. In this regard, our work is to study stability of modern encryption systems. Our strongest practical result is successful logical cryptanalysis (i.e. in the form of SAT problem) of the keystream generator that is used in well-known cipher A5/1. This result was obtained in 2009 with the use of BNB-Grid (paper in journal of ISA RAS, paper on Arxiv, paper in Lecture Notes in Computer Science). In 2010-2011, there were investigations (see, for example, this source), in which real cryptanalysis of A5/1 was also carried out, but using different methods. In fact, an advanced technique of rainbow tables was used. But even the best rainbow tables do not cover all the key space to 100%. Therefore, in the nearest future, we plan to solve in the project SAT@home problems of search for initialization sequences for A5/1 that are not covered by the best known rainbow tables.

Further we plan to use SAT@home to study other cryptographic functions and solve some 'extremely hard' problems of discrete optimization, in particular the Quadratic Assignment Problem (QAP), and some bioinformatics problems (analysis of discrete models of gene networks).