Using Monte Carlo Method for Searching Partitionings of Hard Variants of Boolean Satisfiability Problem

详细信息    查看全文

• 关键词：Monte carlo method ; SAT ; Partitioning ; Tabu search ; Cryptanalysis
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9251
• 期：1
• 页码：222-230
• 全文大小：194 KB
• 参考文献：1.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)
  2. Biryukov, A., Shamir, A., Wagner, D.: Real time cryptanalysis of A5/1 on a PC. In: Schneier, B. (ed.) FSE 2000. LNCS, vol. 1978, pp. 1鈥?8. Springer, Heidelberg (2001) View Article
  3. De Canni猫re, C.: Trivium: a stream cipher construction inspired by block cipher design principles. In: Katsikas, S.K., L贸pez, J., Backes, M., Gritzalis, S., Preneel, B. (eds.) ISC 2006. LNCS, vol. 4176, pp. 171鈥?86. Springer, Heidelberg (2006) View Article
  4. 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鈥?6. Springer, Heidelberg (2008) View Article
  5.Glover, F., Laguna, M.: Tabu Search. Kluwer Academic Publishers, NewYork (1997)View Article MATH
  6.Hyv盲rinen, A.E.J.: Grid Based Propositional Satisfiability Solving. Ph.d. thesis, Aalto University (2011)
  7.Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere et al. [1], pp. 131鈥?53
  8.Metropolis, N., Ulam, S.: The monte carlo method. J. Amer. statistical assoc. 44(247), 335鈥?41 (1949)MathSciNet View Article MATH
  9.Otpuschennikov, I., Semenov, A., Kochemazov, S.: Transalg: a tool for translating procedural descriptions of discrete functions to SAT (tool paper). CoRR abs/1405.1544 (2014)
  10. 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鈥?83. Springer, Heidelberg (2011) View Article
  11. Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244鈥?57. Springer, Heidelberg (2009) View Article
  
• 作者单位：Alexander Semenov (14)
  Oleg Zaikin (14)
  
  14. Institute for System Dynamics and Control Theory SB RAS, Irkutsk, Russia
  
• 丛书名：Parallel Computing Technologies
• ISBN：978-3-319-21909-7
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

In this paper we propose the approach for constructing partitionings of hard variants of the Boolean satisfiability problem (SAT). Such partitionings can be used for solving corresponding SAT instances in parallel. We suggest the approach based on the Monte Carlo method for estimating time of processing of an arbitrary partitioning. We solve the problem of search for a partitioning with good effectiveness via the optimization of the special predictive function over the finite search space. For this purpose we use the tabu search strategy. In our computational experiments we found partitionings for SAT instances encoding problems of inversion of some cryptographic functions. Several of these SAT instances with realistic predicted solving time were successfully solved on a computing cluster and in the volunteer computing project SAT@home. The solving time agrees well with estimations obtained by the proposed method.