Abstract
In order to classify the indeterministic termination behavior of the open source SAT solver CryptoMiniSat in multi-threading mode while processing hard to solve Boolean satisfiability problem instances, internal solver runtime parameters have been collected and analyzed. A subset of these parameters have been selected and employed as features vector to successfully create a machine learning model for the binary classification of the solver’s termination behavior with any single new solving run of a not yet solved instance. The model can be used for the early estimation of a solving attempt as belonging or not belonging to the class of candidates with good chances for a fast termination. In this context, a combination of active profiles of runtime characteristics appear to mirror the influence of the solver’s momentary heuristics on the immediate quality of the solver’s resolution process. Because runtime parameters of already the first two solving iterations are enough to forecast termination of the attempt with good success scores, the results of the present work deliver a promising basis which can be further developed in order to enrich CryptoMiniSat or generally any modern SAT solver with AI abilities.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
SAT – satisfiablity.
- 2.
ML – machine learning.
- 3.
CNF – conjunctive normal form; KPA – known-plaintext attacks.
- 4.
CMS – CryptoMiniSat.
- 5.
AAC – automatic algorithm configuration.
- 6.
CDCL – conflict driven clause learning.
- 7.
NN – neural network.
References
Armando, A., Compagna, L.: SAT-based model-checking for security protocols analysis. Int. J. Inf. Sec. 7(1), 3–32 (2006)
Biere, A., Fröhlich, A.: Evaluating CDCL restart schemes. In: Proceedings of the International Workshop on Pragmatics of SAT (POS 2015), 16 p. (2015). http://fmv.jku.at/papers/BiereFroehlich-POS15.pdf
Chollet, F., et al.: Keras (2015). https://keras.io
Devlin, D., O’Sullivan, B.: Satisfiability as a classification problem. In: Proceedings of the 19th Irish Conference on Artificial Intelligence and Cognitive Science (2008). http://www.cs.ucc.ie/~osullb/pubs/classification.pdf
Ganesh, V.: Machine Learning for SAT Solvers. Abstract. (2018) https://uwaterloo.ca/artificial-intelligence-institute/events/machine-learning-sat-solvers. Invited talk at Waterloo AI Institute, University of Waterloo, Canada
Hughes, G., Bultan, T.: Automated verification of access control policies using a SAT solver. Int. J. Softw. Tools Technol. Transf. 10(6), 503–520 (2008)
Hutter, F., Xu, L., Hoos, H.H., Leyton-Brown, K.: Algorithm runtime prediction: methods & evaluation. Artif. Intell. 206, 79–111 (2014)
Järvisalo, M.: Boolean satisfiability and beyond: algorithms, analysis, and AI applications. In: Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), pp. 4066–4069. AAAI Press (2016). http://www.ijcai.org/Proceedings/16/Papers/602.pdf
Kehui, W., Tao, W., Xinjie, Z., Huiying, L.: CryptoMiniSAT solver based algebraic side-channel attack on PRESENT. In: 2011 First International Conference on Instrumentation, Measurement, Computer, Communication and Control, pp. 561–565 (2011)
Lafitte, F., Nakahara Jr., J., Van Heule, D.: Applications of SAT solvers in cryptanalysis: finding weak keys and preimages. J. Satisfiability Boolean Model. Comput. 9, 1–25 (2014)
Leventi-Peetz, A., Zendel, O., Lennartz, W., Weber, K.: CryptoMiniSat switches-optimization for solving cryptographic instances. In: Proceedings of the International Workshop on Pragmatics of SAT (POS 2018) (2018). https://easychair.org/publications/preprint/Q4kv
Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Theory and Applications of Satisfiability Testing - SAT 2016, Bordeaux, France, Proceedings, pp. 123–140 (2016)
Liang, J.H., Oh, C., Mathews, M., Thomas, C., Li, C., Ganesh, V.: A machine learning based restart policy for CDCL SAT solvers. In: Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT 2018), pp. 94–110. Springer (2018)
Lindauer, M., Eggensperger, K., Feurer, M., Falkner, S., Biedenkapp, A., Hutter, F.: SMAC v3: algorithm configuration in python (2017). https://github.com/automl/SMAC3
Lorenz, C., Schnor, B.: Policy anomaly detection for distributed IPv6 firewalls. In: Proceedings of the 12th International Conference on Security and Cryptography (SECRYPT-2015), pp. 210–219. Science and Technology Publications (2015)
Mauro, J., Nieke, M., Seidl, C., Yu, I.C.: Anomaly detection and explanation in context-aware software product lines. In: Proceedings of the 21st International Systems and Software Product Line Conference, SPLC 2017, Volume B, Sevilla, Spain, pp. 18–21 (2017). https://www.isf.cs.tu-bs.de/cms/team/nieke/papers/2017-SPLC.pdf
Otpuschennikov, I., Semenov, A., Gribanova, I., Zaikin, O., Kochemazov, S.: Encoding Cryptographic Functions to SAT Using Transalg System. arXiv:1607.00888 (2016)
Rintanen, J.: Solving AI Planning Problems with SAT (2013). http://www.epcl-study.eu/content/downloads/slides/rintanen_2013.pdf. Research talk at the EPCL Basic Training Camp
Semenov, A.A., Zaikin, O., Otpuschennikov, I.V., Kochemazov, S., Ignatiev, A.: On cryptographic attacks using backdoors for SAT. In: Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), New Orleans, Louisiana, USA, 2018, pp. 6641–6648 (2018)
Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Theory and Applications of Satisfiability Testing - SAT2009, 12th International Conference, SAT 2009, Swansea, UK, 30 June–3 July, 2009. Proceedings, pp. 244–257 (2009).https://github.com/msoos/cryptominisat
Vanhoef, M., Piessens, F.: Symbolic execution of security protocol implementations: handling cryptographic primitives. In: USENIX Workshop on Offensive Technology (USENIX WOOT) (2018). https://papers.mathyvanhoef.com/woot2018.pdf
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Leventi-Peetz, A.M., Peetz, JV., Rohde, M. (2020). ML Supported Predictions for SAT Solvers Performance. In: Arai, K., Bhatia, R., Kapoor, S. (eds) Proceedings of the Future Technologies Conference (FTC) 2019. FTC 2019. Advances in Intelligent Systems and Computing, vol 1069. Springer, Cham. https://doi.org/10.1007/978-3-030-32520-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-32520-6_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-32519-0
Online ISBN: 978-3-030-32520-6
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)