Technology for translating combinatorial problems into Boolean equations

I. V. Otpuschennikov ; A. A. Semenov

Prikladnaâ diskretnaâ matematika, no. 1 (2011), pp. 96-115.

Résumé

The article is 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.

Détail

Keywords: discrete functions, Boolean equations, cryptoanalysis, propositional encoding.

Bibliographie

[1] Rudeanu S., Boolean functions and equations, North-Holland Publishing Company, Amsterdam–London, 1974, 442 pp. | MR | Zbl

[2] Prestwich S., “CNF encodings”, Handbook of Satisfiability, eds. A. Biere, M. Heule, H. van Maaren, T. Walsh, IOS Press, 2009, 75–97

[3] Cook S. A., “The complexity of theorem-proving procedures”, Proc. 3rd Ann. ACM Symp. on Theory of Computing (STOC 71), ACM, 1971, 151–159

[4] Garey M. R., Johnson S., Computers and intractability: A guide to the theory of NP-completeness, W. H. Freeman, 1979, 340 pp. | MR | Zbl

[5] Semënov A. A., “Translyatsiya algoritmov vychisleniya diskretnykh funktsii v vyrazheniya propozitsionalnoi logiki”, Prikladnye algoritmy v diskretnom analize, Diskretnyi analiz i informatika, 2, 2008, 70–98

[6] Shepherdson J. C., Sturgis H. E., “Computability of recursive functions”, J. Assoc. Comp. Machinery, 10 (1963), 217–255 | MR | Zbl

[7] Katlend N., Vychislimost. Vvedenie v teoriyu rekursivnykh funktsii, Mir, M., 1983, 256 pp. | MR

[8] Tseitin G. S., “O slozhnosti vyvoda v ischislenii vyskazyvanii”, Zapiski nauchnykh seminarov LOMI AN SSSR, 8, 1968, 234–259 | MR | Zbl

[9] Semënov A. A., “O preobrazovaniyakh Tseitina v logicheskikh uravneniyakh”, Prikladnaya diskretnaya matematika, 2009, no. 4, 28–50

[10] Akho A., Seti R., Ulman Dzh., Kompilyatory. Printsipy, tekhnologii, instrumenty, Vilyams, M.–SPb.–Kiev, 2001, 768 pp.

[11] Menezes A., Oorschot P., Vanstone S., Handbook of Applied Cryptography, CRC Press, 1996, 657 pp.

[12] Cook S. A., Mitchel G., “Finding hard instances of the satisfiability problem: A survey”, DIMACS Ser. Discr. Mathem. Theoret. Comp. Scie., 35 (1997), 1–17 | MR | Zbl

[13] Massacci F., Marraro L., “Logical Cryptanalysis as a SAT Problem”, J. Autom. Reas., 24:1–2 (2000), 165–203 | DOI | MR | Zbl

[14] Semënov A. A., Zaikin O. S., Bespalov D. V., Ushakov A. A., “SAT-podkhod v kriptoanalize nekotorykh sistem potochnogo shifrovaniya”, Vychislitelnye tekhnologii, 13:6 (2008), 134–150 | Zbl

[15] Posypkin M. A., Zaikin O. S., Bespalov D. V., Semënov A. A., “Reshenie zadach kriptoanaliza potochnykh shifrov v raspredelennykh vychislitelnykh sredakh”, Trudy ISA RAN, 46, 2009, 119–137

[16] Rueppel R., “Correlation immunity and the summation generator”, LNCS, 218, 1986, 260–272

[17] Schneier B., Applied Cryptography, Protocols, Algorithms, and Source Code in C, Second Edition, John Wiley and Sons, 1996, 758 pp.

[18] Massacci F., Marraro L., Logical Cryptoanalysis as a SAT Problem: the Encoding of the Data Encryption Standard, Preprint, Dipartimento di Imformatica e Sistemistica, Universita di Roma “La Sapienza”, 1999 | MR

[19] embedded.eecs.berkeley.edu/pubs/downloads/espresso

[20] www.cril.univ-artois.fr/PB10/

[21] Een N., Sorensson N., “Translating Pseudo-Boolean Constraints into SAT”, J. Satisfiab., Bool. Model. Comp., 2 (2006), 1–25

[22] MIPLIB – Mixed Integer Problem Library, miplib.zib.de

[23] minisat.se/MiniSat+.html

[24] N. A. Kolchanov, S. S. Goncharov, V. A. Likhoshvai, V. A. Ivanisenko (red.), Sistemnaya kompyuternaya biologiya, Izd-vo SO RAN, Novosibirsk, 2008, 767 pp.

[25] Ganai M., Gupta A., SAT-based scalable formal verification solutions, Springer, 2007, 326 pp. | MR | Zbl