Top

Published in:

2021 | OriginalPaper | Chapter

Finding Effective SAT Partitionings Via Black-Box Optimization

Authors : Alexander Semenov, Oleg Zaikin, Stepan Kochemazov

Published in: Black Box Optimization, Machine Learning, and No-Free Lunch Theorems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

In the present chapter we study one method for partitioning hard instances of the Boolean satisfiability problem (SAT). It uses a subset of a set of variables of an original formula to partition it into a family of subproblems that are significantly easier to solve individually. While it is usually very hard to estimate the time required to solve a hard SAT instance without actually solving it, the partitionings of the presented kind make it possible to naturally construct such estimations via the well-known Monte Carlo method. We show that the problem of finding a SAT partitioning with minimal estimation of time required to solve all subproblems can be formulated as the problem of minimizing a special pseudo-Boolean black-box function. The experimental part of the paper clearly shows that in the context of the proposed approach relatively simple black-box optimization algorithms show good results in application to minimization of the functions of the described kind even when faced with hard SAT instances that encode problems of finding preimages of cryptographic functions.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Non-lattice Covering and Quantization of High Dimensional Sets

next chapter The No Free Lunch Theorem: What Are its Main Implications for the Optimization Practice?

https://github.com/Nauchnik/pdsat.

https://github.com/Nauchnik/alias.

https://github.com/lytr777/CryptoEv.

Irkutsk Supercomputer Center of SB RAS, http://hpc.icc.ru.

Audet, C., Hare, W.: Derivative-Free and Blackbox Optimization. Springer Series in Operations Research and Financial Engineering, Springer, Berlin (2017). https://doi.org/10.1007/978-3-319-68913-5

Babenko, L.K., Maro, E.A., Anikeev, M.V.: Application of algebraic cryptanalysis to MAGMA and PRESENT block encryption standards. In: Proceedings of IEEE 11th International Conference on Application of Information and Communication Technologies (AICT), pp. 1–7 (2017). https://doi.org/10.1109/ICAICT.2017.8686954

Balyo, T., Sinz, C.: Parallel satisfiability. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 3–29. Springer, Berlin (2018). https://doi.org/10.1007/978-3-319-63516-3_1 CrossRef

Bard, G.V.: Algebraic Cryptanalysis, 1st edn. Springer, Berlin (2009)MATHCrossRef

Bessiere, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit complexity and decompositions of global constraints. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence - IJCAI’09, pp. 412–418 (2009)

Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)

Biryukov, A., Shamir, A., Wagner, D.A.: Real time cryptanalysis of A5/1 on a PC. In: Schneier, B. (ed.) Fast Software Encryption, 7th International Workshop, FSE 2000. Lecture Notes in Computer Science, vol. 1978, pp. 1–18. Springer, Berlin (2000). https://doi.org/10.1007/3-540-44706-7_1

Boros, E., Hammer, P.L.: Pseudo-Boolean optimization. Discrete Appl. Math. 123(1–3), 155–225 (2002)MathSciNetMATHCrossRef

Bouillaguet, C., Derbez, P., Fouque, P.: Automatic search of attacks on round-reduced AES and applications. In: Rogaway, P. (ed.) Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology Conference. Lecture Notes in Computer Science, vol. 6841, pp. 169–187. Springer, Berlin (2011). https://doi.org/10.1007/978-3-642-22792-9_10 CrossRef

10.

Cannière, C.D., Preneel, B.: Trivium. In: Robshaw, M.J.B., Billet, O. (eds.) New Stream Cipher Designs - The eSTREAM Finalists. Lecture Notes in Computer Science, vol. 4986, pp. 244–266. Springer, Berlin (2008)CrossRef

11.

Carter, K., Foltzer, A., Hendrix, J., Huffman, B., Tomb, A.: SAW: the software analysis workbench. In: Boleng, J., Taft, S.T. (eds.) Proceedings of the 2013 ACM SIGAda Annual Conference on High Integrity Language Technology, HILT, pp. 15–18. ACM, New York (2013). https://doi.org/10.1145/2527269.2527277 CrossRef

12.

Chang, C.L., Lee, R.C.T.: Symbolic Logic and Mechanical Theorem Proving, 1st edn. Academic Press, Cambridge (1997)MATH

13.

Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004. Lecture Notes in Computer Science, vol. 2988, pp. 168–176. Springer, Berlin (2004). https://doi.org/10.1007/978-3-540-24730-2_15

14.

Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151–158 (1971)

15.

Cook, S.A., Mitchell, D.G.: Finding hard instances of the satisfiability problem: a survey. In: Satisfiability Problem: Theory and Applications. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, pp. 1–18. American Mathematical Society, Providence (1996)

16.

Courtois, N.T.: Algebraic complexity reduction and cryptanalysis of GOST. IACR Cryptol. ePrint Arch. 2011, 626 (2011). http://eprint.iacr.org/2011/626

17.

Courtois, N.T., Gawinecki, J.A., Song, G.: Contradiction immunity and guess-then-determine attacks on GOST. Tatra Mt. Math. Publ. 53(1), 2–13 (2012)MathSciNetMATH

18.

Daemen, J., Rijmen, V.: The Design of Rijndael: AES - The Advanced Encryption Standard. Information Security and Cryptography. Springer, Berlin (2002). https://doi.org/10.1007/978-3-662-04722-4

19.

Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Log. Program. 1(3), 267–284 (1984)MathSciNetMATHCrossRef

20.

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Selected Revised Papers. Lecture Notes in Computer Science, vol. 2919, pp. 502–518. Springer, Berlin (2003). https://doi.org/10.1007/978-3-540-24605-3_37 MATH

21.

Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543–560 (2003)MATHCrossRef

22.

Eibach, T., Pilz, E., Völkel, G.: Attacking Bivium using SAT solvers. In: Büning, H.K., Zhao, X. (eds.) Theory and Applications of Satisfiability Testing - SAT 2008, 11th International Conference, SAT 2008. Lecture Notes in Computer Science, vol. 4996, pp. 63–76. Springer, Berlin (2008). https://doi.org/10.1007/978-3-540-79719-7_7 MATH

23.

Feller, W.: An Introduction to Probability Theory and Its Applications, Volume II. Wiley, New York (1971)

24.

Franco, J., Martin, J.: A history of satisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 3–74. IOS Press, Amsterdam (2009)

25.

Garey, M.R., Johnson, D.S.: Computers and Intractability, vol. 174. Freeman, New York (1979)MATH

26.

Glover, F.: Future paths for integer programming and links to artificial intelligence. Comput. OR 13(5), 533–549 (1986)MathSciNetMATHCrossRef

27.

Gomes, C.P., Sabharwal, A.: Exploiting runtime variation in complete solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 271–288. IOS Press, Amsterdam (2009)

28.

Günther, C.G.: Alternating step generators controlled by de Bruijn sequences. In: Chaum, D., Price, W.L. (eds.) Advances in Cryptology - EUROCRYPT’87, Workshop on the Theory and Application of Cryptographic Techniques. Lecture Notes in Computer Science, vol. 304, pp. 5–14. Springer, Berlin (1987). https://doi.org/10.1007/3-540-39118-5_2

29.

Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel SAT solver. J. Satisf. Boolean Model. Comput. 6(4), 245–262 (2009)MATH

30.

Hamming, R.W.: Error detecting and error correcting codes. Bell Syst. Tech. J. 29(2), 147–160 (1950). https://doi.org/10.1002/j.1538-7305.1950.tb00463.x MathSciNetMATHCrossRef

31.

Hell, M., Johansson, T., Maximov, A., Meier, W.: The Grain family of stream ciphers. In: Robshaw, M.J.B., Billet, O. (eds.) New Stream Cipher Designs - The eSTREAM Finalists. Lecture Notes in Computer Science, vol. 4986, pp. 179–190. Springer, Berlin (2008)CrossRef

32.

Heule, M., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Lourenço, J., Shehory, O. (eds.) Hardware and Software: Verification and Testing - 7th International Haifa Verification Conference, HVC 2011. Lecture Notes in Computer Science, vol. 7261, pp. 50–65. Springer, Berlin (2011). https://doi.org/10.1007/978-3-642-34188-5_8

33.

Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) Theory and Applications of Satisfiability Testing – SAT 2016. Lecture Notes in Computer Science, vol. 9710, pp. 228–245. Springer, Berlin (2016)CrossRef

34.

Hyvärinen, A.E.J.: Grid based propositional satisfiability solving. Ph.D. Thesis, Aalto University (2011)

35.

Hyvärinen, A.E.J., Junttila, T.A., Niemelä, I.: Partitioning SAT instances for distributed solving. In: Fermüller, C.G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17, pp. 372–386. Springer, Berlin (2010). https://doi.org/10.1007/978-3-642-16242-8_27 MATHCrossRef

36.

Janicic, P.: URSA: a system for uniform reduction to SAT. Log. Meth. Comput. Sci. 8(3), 1–39 (2012)MathSciNetMATHCrossRef

37.

Järvisalo, M., Junttila, T.: Limitations of restricted branching in clause learning. Constraints 14(3), 325–356 (2009)MathSciNetMATHCrossRef

38.

Järvisalo, M., Biere, A., Heule, M.: Simulating circuit-level simplifications on CNF. J. Autom. Reason. 49(4), 583–619 (2012)MathSciNetMATHCrossRef

39.

Kirkpatrick, S., Gelatt, C.D., Vecchi, M.P.: Optimization by simulated annealing. Science 220(4598), 671–680 (1983)MathSciNetMATHCrossRef

40.

Kochemazov, S., Zaikin, O.: ALIAS: a modular tool for finding backdoors for SAT. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) Theory and Applications of Satisfiability Testing - 21st International Conference, SAT 2018. Lecture Notes in Computer Science, vol. 10929, pp. 419–427. Springer, Berlin (2018). https://doi.org/10.1007/978-3-319-94144-8_25 MATHCrossRef

41.

Kolda, T.G., Lewis, R.M., Torczon, V.: Optimization by direct search: new perspectives on some classical and modern methods. SIAM Rev. 45(3), 385–482 (2003)MathSciNetMATHCrossRef

42.

Kroening, D.: Software verification. In: Biere et al. [6], pp. 505–532

43.

Lafitte, F.: Cryptosat: a tool for SAT-based cryptanalysis. IET Inf. Secur. 12(6), 463–474 (2018). https://doi.org/10.1049/iet-ifs.2017.0176 CrossRef

44.

Levin, L.: Universal sequential search problems. Probl. Inf. Transm. 9, 265–266 (1973)

45.

Luke, S.: Essentials of Metaheuristics, 2nd edn. Lulu, Morrisville (2013). http://cs.gmu.edu/~sean/book/metaheuristics/

46.

Marques-Silva, J.P., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Rutenbar, R.A., Otten, R.H.J.M. (eds.) Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1996, pp. 220–227. IEEE Computer Society/ACM, New York (1996). https://doi.org/10.1109/ICCAD.1996.569607

47.

Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131–153. IOS Press, Amsterdam (2009)

48.

Maximov, A., Biryukov, A.: Two trivial attacks on trivium. In: Adams, C.M., Miri, A., Wiener, M.J. (eds.) Selected Areas in Cryptography, 14th International Workshop, SAC 2007, Revised Selected Papers. Lecture Notes in Computer Science, vol. 4876, pp. 36–55. Springer, Berlin (2007). https://doi.org/10.1007/978-3-540-77360-3_3

49.

Mcdonald, C., Charnes, C., Pieprzyk, J.: Attacking Bivium with MiniSat. Tech. Rep. 2007/040, ECRYPT Stream Cipher Project (2007)

50.

Menezes, A.J., Vanstone, S.A., Oorschot, P.C.V.: Handbook of Applied Cryptography, 1st edn. CRC Press, Boca Raton (1996)MATH

51.

Metropolis, N., Ulam, S.: The Monte Carlo Method. J. Am. Stat. Assoc. 44(247), 335–341 (1949)MATHCrossRef

52.

Mühlenbein, H.: How genetic algorithms really work: mutation and hillclimbing. In: Männer, R., Manderick, B. (eds.) Parallel Problem Solving from Nature 2, PPSN-II, pp. 15–26. Elsevier, Amsterdam (1992)

53.

Otpuschennikov, I.V., Semenov, A.A., Gribanova, I., Zaikin, O., Kochemazov, S.: Encoding cryptographic functions to SAT using TRANSALG system. In: Kaminka, G.A., Fox, M., Bouquet, P., Hüllermeier, E., Dignum, V., Dignum, F., van Harmelen, F. (eds.) ECAI 2016 - 22nd European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, vol. 285, pp. 1594–1595. IOS Press, Amsterdam (2016). https://doi.org/10.3233/978-1-61499-672-9-1594

54.

Pavlenko, A., Buzdalov, M., Ulyantsev, V.: Fitness comparison by statistical testing in construction of SAT-based guess-and-determine cryptographic attacks. In: Auger, A., Stützle, T. (eds.) Proceedings of the Genetic and Evolutionary Computation Conference, GECCO 2019, pp. 312–320 (2019). https://doi.org/10.1145/3321707.3321847

55.

Pavlenko, A., Semenov, A.A., Ulyantsev, V.: Evolutionary computation techniques for constructing SAT-based attacks in algebraic cryptanalysis. In: Kaufmann, P., Castillo, P.A. (eds.) Applications of Evolutionary Computation - 22nd International Conference, EvoApplications 2019. Lecture Notes in Computer Science, vol. 11454, pp. 237–253. Springer, Berlin (2019). https://doi.org/10.1007/978-3-030-16692-2_16

56.

Posypkin, M., Semenov, A.A., Zaikin, O.: Using BOINC desktop grid to solve large scale SAT problems. Comput. Sci. (AGH) 13(1), 25–34 (2012)

57.

Rios, L., Sahinidis, N.: Derivative-free optimization: a review of algorithms and comparison of software implementations. J. Global Optim. 56, 1247–1293 (2013). https://doi.org/10.1007/s10898-012-9951-y MathSciNetMATHCrossRef

58.

Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965). https://doi.org/10.1145/321250.321253 MathSciNetMATHCrossRef

59.

Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 3rd edn. Prentice Hall, Upper Saddle River (2009)

60.

Semenov, A.: Decomposition representations of logical equations in problems of inversion of discrete functions. J. Comput. Syst. Sci. Int. 48, 718–731 (2009)MathSciNetMATHCrossRef

61.

Semenov, A.A., Zaikin, O.: Using Monte Carlo method for searching partitionings of hard variants of Boolean satisfiability problem. In: Malyshkin, V. (ed.) Parallel Computing Technologies - 13th International Conference, PaCT 2015. Lecture Notes in Computer Science, vol. 9251, pp. 222–230. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-21909-7_21

62.

Semenov, A.A., Zaikin, O.: On the accuracy of statistical estimations of SAT partitionings effectiveness in application to discrete function inversion problems. In: Kononov, A.V., Bykadorov, I.A., Khamisov, O.V., Davydov, I.A., Kononova, P.A. (eds.) Supplementary Proceedings of the 9th International Conference on Discrete Optimization and Operations Research and Scientific School (DOOR 2016). CEUR Workshop Proceedings, vol. 1623, pp. 261–275. CEUR-WS.org (2016)

63.

Semenov, A., Zaikin, O.: Algorithm for finding partitionings of hard variants of Boolean satisfiability problem with application to inversion of some cryptographic functions. SpringerPlus 5(1), 1–16 (2016)CrossRef

64.

Semenov, A.A., Zaikin, O., Bespalov, D., Posypkin, M.: Parallel logical cryptanalysis of the generator A5/1 in BNB-grid system. In: Malyshkin, V. (ed.) Parallel Computing Technologies - 11th International Conference, PaCT 2011. Lecture Notes in Computer Science, vol. 6873, pp. 473–483. Springer, Berlin (2011). https://doi.org/10.1007/978-3-642-23178-0_43 MATH

65.

Semenov, A.A., Zaikin, O., Otpuschennikov, I.V., Kochemazov, S., Ignatiev, A.: On cryptographic attacks using backdoors for SAT. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18), pp. 6641–6648. AAAI Press, Palo Alto (2018)

66.

Semenov, A., Otpuschennikov, I., Gribanova, I., Zaikin, O., Kochemazov, S.: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. Log. Meth. Comput. Sci. 16, 29:1–29:42 (2020)

67.

Soos, M.: Grain of Salt - an automated way to test stream ciphers through SAT solvers. In: Tools’10: Proceedings of the Workshop on Tools for Cryptanalysis, pp. 131–144 (2010)

68.

Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009. Lecture Notes in Computer Science, vol. 5584, pp. 244–257. Springer, Berlin (2009). https://doi.org/10.1007/978-3-642-02777-2_24

69.

Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: A.O. Slisenko (ed.) Studies in Mathematics and Mathematical Logic, Part II, pp. 115–125. Steklov Mathematical Institute, Moscow (1968)

70.

Wegener, I.: The Complexity of Boolean Functions. Wiley, Hoboken (1987)MATH

71.

Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: Gottlob, G., Walsh, T. (eds.) Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, IJCAI-03, pp. 1173–1178. Morgan Kaufmann, Burlington (2003)

72.

Zaikin, O.: SAT-based cryptanalysis: from parallel computing to volunteer computing. In: Voevodin, V.V., Sobolev, S. (eds.) Supercomputing - 5th Russian Supercomputing Days, RuSCDays 2019. Communications in Computer and Information Science, vol. 1129, pp. 701–712. Springer, Berlin (2019). https://doi.org/10.1007/978-3-030-36592-9_57

73.

Zaikin, O., Kochemazov, S.: An improved SAT-based guess-and-determine attack on the alternating step generator. In: Nguyen, P.Q., Zhou, J. (eds.) Information Security - 20th International Conference, ISC 2017. Lecture Notes in Computer Science, vol. 10599, pp. 21–38. Springer, Berlin (2017). https://doi.org/10.1007/978-3-319-69659-1_2

74.

Zaikin, O., Kochemazov, S.: Pseudo-boolean black-box optimization methods in the context of divide-and-conquer approach to solving hard SAT instances. In: OPTIMA 2018 (Supplementary Volume), pp. 76–87. DEStech Publications, Lancaster (2018)

75.

Zaikin, O., Kochemazov, S.: On black-box optimization in divide-and-conquer SAT solving. Optimization Methods and Software pp. 1–25 (2019). https://doi.org/10.1080/10556788.2019.1685993

76.

Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems. J. Symb. Comput. 21(4), 543–560 (1996). https://doi.org/10.1006/jsco.1996.0030 MathSciNetMATHCrossRef

Title: Finding Effective SAT Partitionings Via Black-Box Optimization
Authors: Alexander Semenov
Oleg Zaikin
Stepan Kochemazov
Publisher: Springer International Publishing
Book: Black Box Optimization, Machine Learning, and No-Free Lunch Theorems
Print ISBN: 978-3-030-66514-2

Electronic ISBN: 978-3-030-66515-9

Copyright Year: 2021
DOI: https://doi.org/10.1007/978-3-030-66515-9_11

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner