×

Using merging variables-based local search to solve special variants of MaxSAT problem. (English) Zbl 1460.90155

Kochetov, Yury (ed.) et al., Mathematical optimization theory and operations research. 19th international conference, MOTOR 2020, Novosibirsk, Russia, July 6–10, 2020. Revised selected papers. Cham: Springer. Commun. Comput. Inf. Sci. 1275, 363-378 (2020).
Summary: In this paper we study the inversion of discrete functions associated with some hard combinatorial problems. Inversion of such a function is considered in the form of a special variant of the well-known MaxSAT problem. To solve the latter we apply the previously developed local search method based on the Merging Variables Principle (MVP). The main novelty is that we combine MVP with evolutionary strategies to leave local extrema generated by Merging Variables Hill Climbing algorithm. The results of computational experiments show the effectiveness of the proposed technique in application to inversion of several cryptographic hash functions and to one problem of combinatorial optimization, which is a variant of the Facility Location Problem.
For the entire collection see [Zbl 1454.90004].

MSC:

90C27 Combinatorial optimization
90C09 Boolean programming
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Ahuja, R.K., Ergun, O., Orlin, J.B., Punnen, A.P.: A survey of very large-scale neighborhood search techniques. Discrete Appl. Math. 123(1-3), 75-102 (2002) · Zbl 1014.68052
[2] Ansotegui, C., Bonet, M.L., Levy, J.: Sat-based MaxSAT algorithms. Artif. Intell. 196, 77-105 (2013) · Zbl 1270.68265
[3] Avella, P., D’Auria, B., Salerno, S., Vasil’ev, I.: A computational study of local search algorithms for Italian high-school timetabling. J. Heuristics 13(6), 543-556 (2007) · Zbl 1144.90451
[4] Berg, J., Demirović, E., Stuckey, P.J.: Core-boosted linear search for incomplete MaxSAT. In: Rousseau, L.-M., Stergiou, K. (eds.) CPAIOR 2019. LNCS, vol. 11494, pp. 39-56. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-19212-9_3 · Zbl 07116684
[5] Bessiere, C., Katsirelos, G., Narodytska, N., Walsh, T.: Circuit complexity and decompositions of global constraints. In: IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, 11-17 July 2009, pp. 412-418 (2009)
[6] Biere, A.: CaDiCaL, lingeling, plingeling, treengeling, YalSAT entering the SAT competition 2017. In: Balyo, T., Heule, M.J.H., Järvisalo, M. (eds.) SAT Competition 2017, vol. B-2017-1, pp. 14-15 (2017)
[7] Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185. IOS Press (2009) · Zbl 1183.68568
[8] Boros, E., Hammer, P.L.: Pseudo-boolean optimization. Discrete Appl. Math. 123(1-3), 155-225 (2002) · Zbl 1076.90032
[9] Burke, E., Kendall, G.: Search Methodologies, 2nd edn. Springer, New York (2014). https://doi.org/10.1007/978-1-4614-6940-7
[10] Chang, C.L., Lee, R.C.T.: Symbolic Logic and Mechanical Theorem Proving, 1st edn. Academic Press Inc, Orlando (1997) · Zbl 0263.68046
[11] Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, 3-5 May 1971, Shaker Heights, Ohio, USA, pp. 151-158 (1971)
[12] Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225-239. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23786-7_19
[13] Doerr, B., Le, H.P., Makhmara, R., Nguyen, T.D.: Fast genetic algorithms. In: Proceedings of the Genetic and Evolutionary Computation Conference. GECCO 2017, pp. 777-784. Association for Computing Machinery (2017)
[14] 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) · Zbl 0593.68062
[15] Droste, S., Jansen, T., Wegener, I.: On the analysis of the (1 + 1) evolutionary algorithm. Theor. Comput. Sci. 276(1-2), 51-81 (2002) · Zbl 1002.68037
[16] Bacchus, F.: CSPs: adding structure to SAT. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 10-10. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_2
[17] Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York (1979) · Zbl 0411.68039
[18] Goldreich, O.: Computational Complexity: A Conceptual Perspective, 1st edn. Cambridge University Press, New York (2008) · Zbl 1154.68056
[19] Gu, J., Purdom, P.W., Franco, J., Wah, B.W.: Algorithms for the satisfiability (sat) problem: a survey. In: DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pp. 19-152. American Mathematical Society (1996) · Zbl 0945.03040
[20] Ignatiev, A., Morgado, A., Manquinho, V., Lynce, I., Marques-Silva, J.: Progression in maximum satisfiability. In: Proceedings of the Twenty-First European Conference on Artificial Intelligence. ECAI 2014, pp. 453-458. IOS Press (2014) · Zbl 1366.68266
[21] Ignatiev, A., Morgado, A., Marques-Silva, J.: RC2: an efficient MaxSAT solver. J. Satisf. Boolean Model. Comput. 11(1), 53-64 (2019)
[22] Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a python toolkit for prototyping with SAT oracles. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 428-437. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94144-8_26 · Zbl 06916321
[23] Laporte, G., Nickel, S., Saldanha da Gama, F. (eds.): Location Science. Springer, Switzerland (2015). https://doi.org/10.1007/978-3-319-13111-5 · Zbl 1329.90003
[24] 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 · Zbl 06807229
[25] Li, C.M., Manyà, F.: MaxSAT, hard and soft constraints. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 613-631. IOS Press (2009)
[26] Luke, S.: Essentials of Metaheuristics, 2nd edn. George Mason University (2015)
[27] MacWilliams, F., Sloane, N.: The Theory of Error-Correcting Codes. North Holland (1983) · Zbl 0369.94008
[28] 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 (2009)
[29] Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman and Hall (1997)
[30] Menezes, A.J., Vanstone, S.A., Oorschot, P.C.V.: Handbook of Applied Cryptography, 1st edn. CRC Press Inc, Boca Raton (1996) · Zbl 0868.94001
[31] Mladenović, N., Hansen, P.: Variable neighborhood search. Comput. Oper. Res. 24(11), 1097-1100 (1997) · Zbl 0889.90119
[32] Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints Int. J. 18(4), 478-534 (2013) · Zbl 1317.90199
[33] Mühlenbein, H.: How genetic algorithms really work: mutation and hillclimbing. In: Parallel Problem Solving from Nature 2, PPSN-II, 28-30 September 1992, Brussels, Belgium, pp. 15-26 (1992)
[34] Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2019)
[35] Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence. AAAI 2014, pp. 2717-2723. AAAI Press (2014)
[36] Pavlenko, A., Semenov, A., Ulyantsev, V.: Evolutionary computation techniques for constructing SAT-based attacks in algebraic cryptanalysis. In: Kaufmann, P., Castillo, P.A. (eds.) EvoApplications 2019. LNCS, vol. 11454, pp. 237-253. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16692-2_16
[37] Russell, S.J., Norvig, P.: Artificial Intelligence - A Modern Approach, Third International Edition. Pearson Education (2010) · Zbl 0835.68093
[38] Semenov, A.A.: Decomposition representations of logical equations in problems of inversion of discrete functions. J. Comput. Syst. Sci. Int. 48, 718-731 (2009) · Zbl 1294.90057
[39] Semenov, A., Otpuschennikov, I., Gribanova, I., Zaikin, O., Kochemazov, S.: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. Logical Methods Comput. Sci. 16(1), 1-42 (2020) · Zbl 07199588
[40] Semenov, A.A.: Merging variables: one technique of search in pseudo-boolean optimization. In: Mathematical Optimization Theory and Operations Research. Communications in Computer and Information Science, vol. 1090, pp. 86-102 (2019) · Zbl 1429.90100
[41] Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, part II, Seminars in Mathematics, pp. 115-125 (1970)
[42] Wegener, I.: Theoretical aspects of evolutionary algorithms. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 64-78. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-48224-5_6
[43] Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: The 18th International Joint Conference on Artificial Intelligence (IJCAI 2003), pp. 1173-1178 (2003)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.