Skip to main content
SpringerLink
Log in
Book cover

International Conference on Mathematical Optimization Theory and Operations Research

MOTOR 2019: Mathematical Optimization Theory and Operations Research pp 402–417Cite as

Black-Box Optimization in an Extended Search Space for SAT Solving

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11548))

Abstract

The Divide-and-Conquer approach is often used to solve hard instances of the Boolean satisfiability problem (SAT). In particular, it implies splitting an original SAT instance into a series of simpler subproblems. If this split satisfies certain conditions, then it is possible to use a stochastic pseudo-Boolean black-box function to estimate the time required for solving an original SAT instance with the chosen decomposition. One can use black-box optimization methods to minimize the function over the space of all possible decompositions. In the present study, we make use of peculiar features which stem from the NP-completeness of the Boolean satisfiability problem to improve this general approach. In particular, we show that the search space over which the black-box function is minimized can be extended by adding solver parameters and the SAT encoding parameters into it. In the computational experiments, we use the SMAC algorithm to optimize such black-box functions for hard SAT instances encoding the problems of cryptanalysis of several stream ciphers. The results show that the proposed approach outperforms the competition.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Ashlock, D.: Evolutionary Computation for Modeling and Optimization, 1st edn. Springer, New York (2010)

    MATH  Google Scholar 

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

    Book  MATH  Google Scholar 

  3. Bard, G.V.: Algebraic Cryptanalysis, 1st edn. Springer, Boston (2009). https://doi.org/10.1007/978-0-387-88757-9

    Book  MATH  Google Scholar 

  4. 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)

    Google Scholar 

  5. Borghoff, J., Knudsen, L.R., Matusiewicz, K.: Hill climbing algorithms and Trivium. In: Biryukov, A., Gong, G., Stinson, D.R. (eds.) SAC 2010. LNCS, vol. 6544, pp. 57–73. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19574-7_4

    Chapter  Google Scholar 

  6. Breiman, L.: Random forests. Mach. Learn. 45(1), 5–32 (2001)

    Article  Google Scholar 

  7. De Cannière, C., Preneel, B.: Trivium. In: Robshaw, M., Billet, O. (eds.) New Stream Cipher Designs - The eSTREAM. LNCS, vol. 4986, pp. 244–266. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68351-3_18

    Chapter  Google Scholar 

  8. Irkutsk supercomputer center of SB RAS. http://hpc.icc.ru

  9. 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)

    MathSciNet  MATH  Google Scholar 

  10. Eibach, T., Pilz, E., Völkel, G.: Attacking bivium using SAT solvers. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 63–76. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79719-7_7

    Chapter  MATH  Google Scholar 

  11. Falkner, S., Lindauer, M., Hutter, F.: SpySMAC: automated configuration and performance analysis of SAT solvers. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 215–222. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_16

    Chapter  MATH  Google Scholar 

  12. Le Frioux, L., Baarir, S., Sopena, J., Kordon, F.: PaInleSS: a framework for parallel SAT solving. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 233–250. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_15

    Chapter  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  14. Günther, C.G.: Alternating step generators controlled by De Bruijn sequences. In: Chaum, D., Price, W.L. (eds.) EUROCRYPT 1987. LNCS, vol. 304, pp. 5–14. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-39118-5_2

    Chapter  Google Scholar 

  15. Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel SAT solver. JSAT 6(4), 245–262 (2009)

    MATH  Google Scholar 

  16. Hansen, P., Mladenović, N.: Variable neighborhood search: principles and applications. Eur. J. Oper. Res. 130(3), 449–467 (2001). https://doi.org/10.1016/S0377-2217(00)00100-4

    Article  MathSciNet  MATH  Google Scholar 

  17. Heule, M.J.H., Kullmann, O., Biere, A.: Cube-and-conquer for satisfiability. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 31–59. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63516-3_2

    Chapter  Google Scholar 

  18. Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Coello, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 507–523. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25566-3_40

    Chapter  Google Scholar 

  19. Hutter, F., Lindauer, M., Balint, A., Bayless, S., Hoos, H., Leyton-Brown, K.: The configurable SAT solver challenge (CSSC). Artif. Intell. 243, 1–5 (2015). https://doi.org/10.1016/j.artint.2016.09.006

    Article  MathSciNet  MATH  Google Scholar 

  20. Hyvärinen, A.E.J., Junttila, T., Niemelä, I.: A distribution method for solving SAT in grids. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 430–435. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_39

    Chapter  Google Scholar 

  21. Jones, D.R., Schonlau, M., Welch, W.J.: Efficient global optimization of expensive black-box functions. J. Glob. Optim. 13(4), 455–492 (1998)

    Article  MathSciNet  Google Scholar 

  22. Kochemazov, S., Zaikin, O.: ALIAS: a modular tool for finding backdoors for SAT. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 419–427. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_25

    Chapter  MATH  Google Scholar 

  23. Lasry, G.: A Methodology for the Cryptanalysis of Classical Ciphers with Search Metaheuristics. Ph.D. thesis, University of Kassel, Germany (2018). http://www.upress.uni-kassel.de/katalog/abstract.php?978-3-7376-0458-1

  24. Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere et al. [4], pp. 131–153

    Google Scholar 

  25. Massacci, F.: Using Walk-SAT and Rel-SAT for cryptographic key search. In: IJCAI 1999, pp. 290–295 (1999)

    Google Scholar 

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

    Google Scholar 

  27. Metropolis, N., Ulam, S.: The Monte Carlo method. J. Amer. statistical assoc. 44(247), 335–341 (1949)

    Article  MathSciNet  Google Scholar 

  28. Nadel, A., Ryvchin, V.: Chronological backtracking. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 111–121. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_7

    Chapter  Google Scholar 

  29. Nossum, V.: SAT-based preimage attacks on SHA-1. Ph.D. thesis, University of OSLO, Department of Informatics (2012)

    Google Scholar 

  30. Otpuschennikov, I., Semenov, A., Gribanova, I., Zaikin, O., Kochemazov, S.: Encoding cryptographic functions to SAT using TRANSALG system. In: ECAI 2016. FAAI, vol. 285, pp. 1594–1595. IOS Press (2016)

    Google Scholar 

  31. Prestwich, S.D.: CNF encodings. In: Biere et al. [4], pp. 75–97

    Google Scholar 

  32. 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)

    Article  Google Scholar 

  33. Semenov, A., Zaikin, O., Bespalov, D., Posypkin, M.: Parallel logical cryptanalysis of the generator A5/1 in BNB-grid system. In: Malyshkin, V. (ed.) PaCT 2011. LNCS, vol. 6873, pp. 473–483. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23178-0_43

    Chapter  MATH  Google Scholar 

  34. Semenov, A., Zaikin, O., Otpuschennikov, I., Kochemazov, S., Ignatiev, A.: On cryptographic attacks using backdoors for SAT. In: AAAI 2018, pp. 6641–6648 (2018)

    Google Scholar 

  35. Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02777-2_24

    Chapter  Google Scholar 

  36. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation (Artificial Intelligence), pp. 466–483. Springer, Heidelberg (1983). https://doi.org/10.1007/978-3-642-81955-1_28

    Chapter  Google Scholar 

  37. Walter, M., Bulygin, S., Buchmann, J.: Optimizing guessing strategies for algebraic cryptanalysis with applications to EPCBC. In: Kutyłowski, M., Yung, M. (eds.) Inscrypt 2012. LNCS, vol. 7763, pp. 175–197. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38519-3_12

    Chapter  Google Scholar 

  38. Whitley, D.: A genetic algorithm tutorial. Stat. Comput. 4(2), 65–85 (1994). https://doi.org/10.1007/BF00175354

    Article  Google Scholar 

  39. Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: IJCAI 2003, pp. 1173–1178 (2003)

    Google Scholar 

  40. Zaikin, O., Kochemazov, S.: An improved SAT-based guess-and-determine attack on the alternating step generator. In: Nguyen, P., Zhou, J. (eds.) ISC 2017. LNCS, vol. 10599, pp. 21–38. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-69659-1_2

    Chapter  Google Scholar 

  41. 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, Inc. (2018)

    Google Scholar 

Download references

Acknowledgements

Authors thank Dr. Alexander Semenov for valuable preliminary discussions regarding the SAT algorithms parameter tuning in the context of Divide-and-Conquer solving. We would also like to thank anonymous reviewers for their valuable comments that made it possible to improve the quality of the present paper. The research was partially supported by Council for Grants of the President of the Russian Federation (grant no. MK-4155.2018.9) and by Russian Foundation for Basic Research (grant no. 19-07-00746-a).

Author information

Authors and Affiliations

  1. ISDCT SB RAS, Irkutsk, Russia

    Oleg Zaikin & Stepan Kochemazov

Authors
  1. Oleg Zaikin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stepan Kochemazov
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Oleg Zaikin .

Editor information

Editors and Affiliations

  1. Krasovsky Institute of Mathematics and Mechanics, Ekaterinburg, Russia

    Michael Khachay

  2. Sobolev Institute of Mathematics, Novosibirsk, Russia

    Yury Kochetov

  3. University of Florida, Gainesville, FL, USA

    Panos Pardalos

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zaikin, O., Kochemazov, S. (2019). Black-Box Optimization in an Extended Search Space for SAT Solving. In: Khachay, M., Kochetov, Y., Pardalos, P. (eds) Mathematical Optimization Theory and Operations Research. MOTOR 2019. Lecture Notes in Computer Science(), vol 11548. Springer, Cham. https://doi.org/10.1007/978-3-030-22629-9_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-22629-9_28

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-22628-2

  • Online ISBN: 978-3-030-22629-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation