On black-box optimization in divide-and-conquer SAT solving

References

• ALIAS a modular tool for finding backdoors for SAT. Available at https://github.com/nauchnik/alias.
   Google Scholar
• C. Audet and W. Hare, Derivative-Free and Blackbox Optimization, Springer Series in Operations Research and Financial Engineering. Springer International Publishing, Berlin, 2017.
   Google Scholar
• S. Babbage and M. Dodd, The MICKEY stream ciphers, in New Stream Cipher Designs – The eSTREAM Finalists, M.J.B. Robshaw and Olivier Billet, eds., Lecture Notes in Computer Science, Vol. 4986, Springer, Berlin, 2008, pp. 191–209.
   Google Scholar
• T. Balyo, A. Biere, M. Iser and C. Sinz, SAT race 2015, Artif. Intell. 241 (2016), pp. 45–65. doi: 10.1016/j.artint.2016.08.007
   Web of Science ®Google Scholar
• G.V. Bard, Algebraic Cryptanalysis, 1st ed., Springer Publishing Company Incorporated, New York, NY, 2009.
   Google Scholar
• A. Biere, M. Heule, H. van Maaren and T. Walsh, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, Vol. 185, IOS Press, Amsterdam, 2009.
   Google Scholar
• C. Blum and A. Roli, Metaheuristics in combinatorial optimization: Overview and conceptual comparison, ACM Comput. Surv. 35(3) (Sep 2003), pp. 268–308. doi: 10.1145/937503.937505
   Web of Science ®Google Scholar
• M. Boesgaard, M. Vesterager, and E. Zenner, The Rabbit stream cipher, in New Stream Cipher Designs – The eSTREAM Finalists, Matthew J.B. Robshaw and Olivier Billet, eds., Lecture Notes in Computer Science, Vol. 4986, Springer, Berlin, 2008, pp. 69–83.
   Google Scholar
• L. Breiman, Random forests, Mach. Learn. 45(1) (2001), pp. 5–32. doi: 10.1023/A:1010933404324
   Web of Science ®Google Scholar
• E. Clarke, D. Kroening, and F. Lerda, A tool for checking ANSI-C programs, in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), K. Jensen and A. Podelski, eds., Lecture Notes in Computer Science, Vol. 2988, Springer, Berlin, 2004, pp. 168–176.
   Google Scholar
• S.A. Cook and D.G. Mitchell, Finding hard instances of the satisfiability problem: A survey, in Satisfiability Problem: Theory and Applications, D.-Z. Du, J. Gu and P.M. Pardalos, eds., DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 35, DIMACS/AMS, Providence, 1996, pp. 1–18.
   Google Scholar
• S.A. Cook, The complexity of theorem-proving procedures, Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3–5, 1971, Shaker Heights, OH, USA, 1971, pp. 151–158.
   Google Scholar
• N.T. Courtois, J.A. Gawinecki, and G. Song, Contradiction immunity and guess-then-determine attacks on GOST, Tatra Mt. Math. Publ. 53(1) (2012), pp. 2–13.
   Google Scholar
• M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Commun. ACM 5(7) (1962), pp. 394–397. doi: 10.1145/368273.368557
   Web of Science ®Google Scholar
• C. De Cannière and B. Preneel, Trivium, in New Stream Cipher Designs – The eSTREAM Finalists, Matthew J.B. Robshaw and Olivier Billet, eds., Lecture Notes in Computer Science, Vol. 4986, Springer, Berlin, 2008, pp. 244–266.
   Google Scholar
• S. Droste, T. Jansen, and I. Wegener, On the analysis of the (1+1) evolutionary algorithm, Theor. Comput. Sci. 276(1–2) (2002), pp. 51–81. doi: 10.1016/S0304-3975(01)00182-7
   Web of Science ®Google Scholar
• T. Eibach, E. Pilz, and G. Völkel, Attacking Bivium using SAT Solvers, in H.K. Bning and X. Zhao, eds., Proceedings of the 11th International Conference on Theory and Applications of Satisfiability Testing, 12–15 May 2008; Guangzhou, China, 2008, pp. 63–76.
   Google Scholar
• eSTREAM: The ECRYPT stream cipher project. Available at http://www.ecrypt.eu.org/stream/.
   Google Scholar
• Yu. G. Evtushenko, S.A. Lurie, M.A. Posypkin and Yu. O. Solyaev, Application of optimization methods for finding equilibrium states of two-dimensional crystals, Comput. Math. Math. Phys. 56(12) (2016), pp. 2001–2010. doi: 10.1134/S0965542516120083
   Web of Science ®Google Scholar
• N. Eén and N. Sörensson, Temporal induction by incremental SAT solving, Electr. Notes Theor. Comput. Sci. 89(4) (2003), pp. 543–560. doi: 10.1016/S1571-0661(05)82542-3
   Google Scholar
• M.R. Garey and D.S. Johnson, Computers and Intractability; A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1990.
   Google Scholar
• M. Gendreau and J-Y. Potvin, Handbook of Metaheuristics, 2nd ed., Springer Publishing Company, Incorporated, New York, NY, 2010.
   Google Scholar
• F. Glover, Future paths for integer programming and links to artificial intelligence, Comput. OR 13(5) (1986), pp. 533–549. doi: 10.1016/0305-0548(86)90048-1
   Google Scholar
• C.G. Günther, Alternating Step Generators Controlled by De Bruijn Sequences, Springer, Berlin, Heidelberg, 1988, pp. 5–14.
   Google Scholar
• R.W. Hamming, Error detecting and error correcting codes, Bell Syst. Tech. J. 29(2) (1950), pp. 147–160. doi: 10.1002/j.1538-7305.1950.tb00463.x
   Google Scholar
• P. Hansen and N. Mladenovi, Variable neighborhood search: Principles and applications, Eur. J. Oper. Res. 130(3) (2001), pp. 449–467. doi: 10.1016/S0377-2217(00)00100-4
   Web of Science ®Google Scholar
• N. Hansen and A. Ostermeier, Adapting arbitrary normal mutation distributions in evolution strategies: The covariance matrix adaptation, Proceedings of 1996 IEEE International Conference on Evolutionary Computation, 1996, pp. 312–317.
   Google Scholar
• M. Hell, T. Johansson, A. Maximov, and W. Meier, The grain family of stream ciphers, in New Stream Cipher Designs-The eSTREAM Finalists, Matthew J.B. Robshaw and Olivier Billet, eds., Lecture Notes in Computer Science, Vol. 4986, Springer, Berlin, 2008, pp. 179–190.
   Google Scholar
• M.J.H. Heule, O. Kullmann, and A. Biere, Cube-and-conquer for satisfiability, in Handbook of Parallel Constraint Reasoning, Springer, New York, NY, 2018, pp. 31–59.
   Google Scholar
• M.J.H. Heule, O. Kullmann, S. Wieringa and A. Biere, Cube and conquer: Guiding CDCL SAT solvers by lookaheads, in Hardware and Software: Verification and Testing, Lecture Notes in Computer Science, Vol. 7261, Springer, Berlin, Heidelberg, 2012, pp. 50–65.
   Google Scholar
• R. Hooke, and T.A. Jeeves, “Direct search” solution of numerical and statistical problems, J. ACM 8(2) (Apr 1961), pp. 212–229. doi: 10.1145/321062.321069
   Google Scholar
• F. Hutter, H.H. Hoos, and K. Leyton-Brown, Sequential model-based optimization for general algorithm configuration. in Proceedings of LION-5, 2011, pp. 507–523.
   Google Scholar
• F. Hutter, H.H. Hoos, and K. Leyton-Brown, Sequential model-based optimization for general algorithm configuration, in Carlos A. Coello Coello, ed., Learning and Intelligent Optimization-5th International Conference, LION 5, Rome, Italy, January 17–21, 2011. Selected Papers, Lecture Notes in Computer Science, Vol. 6683, Springer, Berlin, 2011, pp. 507–523.
   Google Scholar
• A.E.J. Hyvärinen, T. Junttila, and I. Niemelä, A distribution method for solving SAT in grids, in Theory and Applications of Satisfiability Testing-SAT 2006, A. Biere and C.P. Gomes, eds., Lecture Notes in Computer Science, Vol. 4121, Springer, Berlin, 2006, pp. 430–435.
   Google Scholar
• A.E.J. Hyvärinen, T.A. Junttila, and I. Niemelä, Partitioning SAT instances for distributed solving, in C.G. Fermüller and A. Voronkov, eds., Logic for Programming, Artificial Intelligence, and Reasoning-17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings, Lecture Notes in Computer Science, Vol. 6397, Springer, Berlin, 2010, pp. 372–386.
   Google Scholar
• Irkutsk supercomputer center of SB RAS. Available at http://hpc.icc.ru.
   Google Scholar
• P. Janicic, URSA: A system for uniform reduction to SAT, Log. Methods Comput. Sci. 8(3) (2012), pp. 1–39. doi: 10.2168/LMCS-8(3:30)2012
   Web of Science ®Google Scholar
• D.R. Jones, M. Schonlau, and W.J. Welch, Efficient global optimization of expensive black-box functions, J. Global Optim. 13(4) (1998), pp. 455–492. doi: 10.1023/A:1008306431147
   Web of Science ®Google Scholar
• S. Kochemazov and O. Zaikin, ALIAS: A modular tool for finding backdoors for SAT, in Theory and Applications of Satisfiability Testing – SAT 2018, 2018, pp. 419–427.
   Google Scholar
• F. Lafitte, Cryptosat: A tool for sat-based cryptanalysis, IET Inform. Sec. 12(6) (2018), pp. 463–474. doi: 10.1049/iet-ifs.2017.0176
   Web of Science ®Google Scholar
• E.L. Lawler and D.E. Wood, Branch-and-bound methods: A survey, Oper. Res. 14(4) (1966), pp. 699–719. doi: 10.1287/opre.14.4.699
   Web of Science ®Google Scholar
• J.P. Marques Silva and K.A. Sakallah, GRASP: A new search algorithm for satisfiability, in Proceedings of the 1996 IEEE/ACM International Conference on Computer-aided Design, ICCAD '96, 1996, pp. 220–227.
   Google Scholar
• F. Massacci and L. Marraro, Logical cryptanalysis as a SAT problem, J. Autom. Reasoning 24(1/2) (2000), pp. 165–203. doi: 10.1023/A:1006326723002
   Web of Science ®Google Scholar
• F. Massacci, Using Walk-SAT and Rel-SAT for cryptographic key search, in IJCAI'99, 1999, pp. 290–295.
   Google Scholar
• A. Maximov and A. Biryukov, Two trivial attacks on trivium, in Selected Areas in Cryptography, Carlisle Adams, Ali Miri, and Michael Wiener, eds., Springer, Berlin, Heidelberg, 2007, pp. 36–55.
   Google Scholar
• C. Mcdonald, C. Charnes, and J. Pieprzyk, Attacking Bivium with MiniSat. Technical Report 2007/040, ECRYPT Stream Cipher Project, 2007.
   Google Scholar
• A.J. Menezes, S.A. Vanstone, and P.C. Van Oorschot, Handbook of Applied Cryptography, 1st ed., CRC Press Inc., Boca Raton, FL, 1996.
   Google Scholar
• N. Metropolis and S. Ulam, The Monte Carlo method, J. Am. Stat. Assoc. 44(247) (1949), pp. 335–341. doi: 10.1080/01621459.1949.10483310
   PubMed Web of Science ®Google Scholar
• I. Otpuschennikov, A. Semenov, I. Gribanova, O. Zaikin and S. Kochemazov, Encoding cryptographic functions to SAT using TRANSALG system, in ECAI 2016-22nd European Conference on Artificial Intelligence, Vol. 285, Frontiers in Artificial Intelligence and Applications, IOS Press, Amsterdam, 2016, pp. 1594–1595.
   Google Scholar
• A. Pavlenko, M. Buzdalov, and V. Ulyantsev, Fitness comparison by statistical testing in construction of sat-based guess-and-determine cryptographic attacks, in A. Auger and T. Stützle, eds., Proceedings of the Genetic and Evolutionary Computation Conference, GECCO 2019, Prague, Czech Republic, July 13–17, 2019, ACM, New York, NY, 2019, pp. 312–320.
   Google Scholar
• A. Pavlenko, A. Semenov, and V. Ulyantsev, Evolutionary computation techniques for constructing sat-based attacks in algebraic cryptanalysis, in Applications of Evolutionary Computation-22nd International Conference, EvoApplications 2019, Held as Part of EvoStar 2019, Leipzig, Germany, April 24–26, 2019, Proceedings, P. Kaufmann and P.A. Castillo, eds., Lecture Notes in Computer Science, Vol. 11454, Springer, Cham, 2019, pp. 237–253.
   Google Scholar
• M.J.B. Robshaw and O. Billet, New stream cipher designs-the eSTREAM Finalists, Lecture Notes in Computer Science, Vol. 4986, Springer, Berlin, 2008.
   Google Scholar
• S. Russell and P. Norvig, Artificial Intelligence: A Modern Approach, 3rd ed., Prentice Hall, Upper Saddle River, NJ, 2009.
   Google Scholar
• A.A. Semenov, I.V. Otpuschennikov, I. Gribanova, O. Zaikin and S. Kochemazov, Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. CoRR, abs/1805.07239, 2018.
   Google Scholar
• A. Semenov and O. Zaikin, Algorithm for finding partitionings of hard variants of Boolean satisfiability problem with application to inversion of some cryptographic functions, SpringerPlus 5(1) (2016), pp. 1–16. doi: 10.1186/s40064-016-2187-4
   PubMedGoogle Scholar
• A. Semenov, O. Zaikin, D. Bespalov and M. Posypkin, Parallel logical cryptanalysis of the generator A5/1 in BNB-grid system, in 11th International Conference on Parallel Computing Technologies-PaCT 2011, Lecture Notes in Computer Science, Vol. 6873, Springer, Berlin, 2011, pp. 473–483.
   Google Scholar
• A. Semenov, O. Zaikin, I. Otpuschennikov, S. Kochemazov and A. Ignatiev, On cryptographic attacks using backdoors for SAT, in The Thirty-Second AAAI Conference on Artificial Intelligence, AAAI'2018, 2018, pp. 6641–6648.
   Google Scholar
• M. Soos, K. Nohl and C. Castelluccia, Extending SAT solvers to cryptographic problems, in Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing: 30 June–3 July, 2009; Swansea, UK, O Kullmann, ed., Springer, Berlin, 2009, pp. 244–257.
   Google Scholar
• G.S. Tseitin, On the complexity of derivation in propositional calculus, in Studies in MATHEMATICS and Mathematical Logic, Part II, A.O. Slisenko, ed., Nauka, Leningrad, 1970, pp. 115–125.
   Google Scholar
• D. Whitley, A genetic algorithm tutorial, Stat. Comput. 4(2) (Jun 1994), pp. 65–85. doi: 10.1007/BF00175354
   Web of Science ®Google Scholar
• T. Yasumoto and T. Okuwaga, Rokk 1.0.1., in SAT Competition 2014, A. Belov, D. Diepold, M. Heule, and M. Järvisalo, eds., University of Helsinki, Helsinki, 2014, p. 70.
   Google Scholar
• O. Zaikin and S. Kochemazov, An improved SAT-based guess-and-determine attack on the alternating step generator, in ISC 2017, Lecture Notes in Computer Science, Vol. 10599, Springer, Cham, 2017, pp. 21–38.
   Google Scholar
• O. Zaikin and S. Kochemazov, Pseudo-boolean black-box optimization methods in the context of divide-and-conquer approach to solving hard SAT instances, in OPTIMA 2018 (Supplementary Volume), DEStech Publications, Inc., Lancaster, PA, 2018, pp. 76–87.
   Google Scholar
• O. Zaikin and S. Kochemazov, Black-box optimization in an extended search space for SAT solving, in Mathematical Optimization Theory and Operations Research-18th International Conference, MOTOR 2019, Ekaterinburg, Russia, July 8–12, 2019, Proceedings, M. Khachay, Y. Kochetov, and P.M. Pardalos, eds., Lecture Notes in Computer Science, Vol. 11548, Springer, Cham, 2019, pp. 402–417.
   Google Scholar
• H. Zhang, M. Paola Bonacina, and J. Hsiang, PSATO: A distributed propositional prover and its application to quasigroup problems, J. Symbol. Comput. 21(4) (1996), pp. 543–560. doi: 10.1006/jsco.1996.0030
   Web of Science ®Google Scholar