Full text of article: Russian language.

Abstract:
The one of the most interesting problem of discrete mathematics is the SAT (satisfiability) problem [9]. Good way in sat solver developing is to transform the SAT problem to the problem of continuous search of global minimums of the functional associated with the CNF. This article proves the special construction of the functional and offers to solve the system of non-linear algebraic equation that determines functional stationary points via modified method of consecutive approximation. The article describes parallel versions of the method. Also gives the schema of using the method to important problems of cryptographic analysis of asymmetric ciphers, including determining the concrete bits of multipliers (in binary form) in large factorization problems.

Key words:
CNF, SAT, resolution, minimization, cryptographic analysis, factorization.

References:

1. Dulkeit, V. I. Minimizing functionals associated with cryptographic analysis problems / V. I. Dulkeit, R.Т. Faizullin, I. G. Khnykin // Differential Equations. Functional Spaces. Theory of Approximations. Proceedings of the international conference to commemorate S. L. Sobolev’s centenary. - Novosibirsk: Institute of Mathematics of the Siberian Branch of the RAS, 2008. - Pp. 484-485 (in Russian).
   
2. Dulkeit, V. I. Reducing of problems of asymmetric cipher cryptoanalysis to solving associated satisfiability problems  / V. I. Dulkeit, R. Т. Faizullin, I. G. Khnykin // Proceedings of the XIII All-Russian conference Mathematical Methods of Pattern Recognition  - Moscow: MAKS Press, 2007. - Pp. 249-251 (in Russian).
   
3. Kreinovich, V. Ya. Semantics of a S. Yu. Maslov iterative method / V. Ya. Kreinovich // Problems of Cybernetics. Problems of search reduction.- Moscow.: USSR Academy of Sciences, 1987. - Pp. 30-62 (in Russian).
   
4. Maslov, S. Yu. Iterative methods in a search model / S. Y. Maslov // Proceedings of IX-th All-Union conference in cybernetics. - Sukhumi, 1981. - Pp. 26 – 28 (in Russian).
   
5. Matiyasevich, V. Yu. Feasible alternative methods for establishing the satisfiability of propositional formulae / V. Yu. Matiaysevich // Problems of Cybernetics. Problems of search reduction.- Moscow: USSR Academy of Sciences. -1987. - Pp. 87-90 (in Russian).
   
6. Oparin, G. А. Continuous models for solving sets of Boolean equations / G. А. Oparin, А. P. Novopashin // Herald of Tomsk State University. -2004. –No. 9 (1) - Pp. 20-25 (in Russian).
   
7. Khnykin, I. G. CNF modifications equivalent to problems of asymmetric cipher cryptoanalysis by a resolution technique / I. G. Khnykin // Information Technology of Modeling and Control. - 2007. No. 2. - Pp. 328-337 (in Russian).
   
8. Cook, S.A. Finding hard instances for the satisfiability problem: / S.A. Cook, D.G. Mitchel //A survey. DIMACS series in discrete mathematics and theoretical computer science. V.5. -1997.
   
9. Cook, S.A. The complexity of theorem proving procedures / S.A. Cook // Proceedings of the Third Annual ACM Sympo-sium on Theory of Computing. - 1971. - P.151-158.
   
10. Gu, J. Algorithms for the satisfiability (sat) problem / J. Gu [and other] / J. Gu //Eds. Ding-Zhu Du Jun Gu and Panos Pardalos. - Satisfiability Problem. Theory and Ap-plications. DIMACS Series in Discrete Mathematics and Theoretical Computer Science.- AMS, 1997. -P. 19-152.
    
11. Koblitz, N. The state of elliptic curve cryptography. / N. Koblitz, A. Menezes, S. Vanstone //Designs Codes and Cryptography, 19, 2000. -P.173-193
    
12. Lenstra, A. The Development of the Number Field Sieve./ A. Lenstra, H. Lenstra -Springer-Verlag, -1993.
    
13. SAT 2005 Competition results [Internet database]. – Free access: http://www.lri.fr/~simon/contest05/results/.
    
14. SAT Live! [Internet database]. – Free access: www.satlive.org.

---

© 2009, ИСОИ РАН
Россия, 443001, Самара, ул. Молодогвардейская, 151; электронная почта: ko@smr.ru ; тел: +7 (846) 332-56-22, факс: +7 (846 2) 332-56-20