×

Generating random SAT instances: multiple solutions could be predefined and deeply hidden. (English) Zbl 1506.68130

Summary: The generation of SAT instances is an important issue in computer science, and it is useful for researchers to verify the effectiveness of SAT solvers. Addressing this issue could inspire researchers to propose new search strategies. SAT problems exist in various real-world applications, some of which have more than one solution. However, although several algorithms for generating random SAT instances have been proposed, few can be used to generate hard instances that have multiple predefined solutions. In this paper, we propose the KHidden-M algorithm to generate SAT instances with multiple predefined solutions that could be hard to solve by the local search strategy when the number of predefined solutions is small enough and the Hamming distance between them is not less than half of the solution length. Specifically, first, we generate an SAT instance that is satisfied by all of the predefined solutions. Next, if the generated SAT instance does not satisfy the hardness condition, then a strategy will be conducted to adjust clauses through multiple iterations to improve the hardness of the whole instance. We propose three strategies to generate the SAT instance in the first part. The first strategy is called the random strategy, which randomly generates clauses that are satisfied by all of the predefined solutions. The other two strategies are called the estimating strategy and greedy strategy, and using them, we attempt to generate an instance that directly satisfies or is closer to the hardness condition for the local search strategy. We employ two SAT solvers (i.e., WalkSAT and Kissat) to investigate the hardness of the SAT instances generated by our algorithm in the experiments. The experimental results show the effectiveness of the random, estimating and greedy strategies. Compared to the state-of-the-art algorithm for generating SAT instances with predefined solutions, namely, M-hidden, our algorithm could be more effective in generating hard SAT instances.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T37 Reasoning under uncertainty in the context of artificial intelligence
Full Text: DOI

References:

[1] Achlioptas, D. (2001). Lower bounds for random 3-SAT via differential equations.Theoretical Computer Science,265(1-2), 159-185. · Zbl 0983.68079
[2] Achlioptas, D., Gomes, C., Kautz, H., & Selman, B. (2000). Generating satisfiable problem instances.AAAI/IAAI,2000, 256-261.
[3] Achlioptas, D., Jia, H., & Moore, C. (2005). Hiding satisfying assignments: Two are better than one.Journal of Artificial Intelligence Research,25, 623-639. · Zbl 1080.68653
[4] Ans´otegui, C., Bonet, M. L., & Levy, J. (2009). Towards industrial-like random sat instances. InProceedings of the 21st International Joint Conference on Artificial Intelligence, p. 387-392.
[5] Ateniese, G., Cristofaro, E. D., & Tsudik, G. (2011). (if) size matters: size-hiding private set intersection. InInternational Workshop on Public Key Cryptography, pp. 156-173. · Zbl 1281.94012
[6] Barak-Pelleg, D., Berend, D., & Saunders, J. (2022). A model of random industrial sat. Theoretical Computer Science,910, 91-112. · Zbl 1535.68179
[7] Barthel, W., Hartmann, A. K., Leone, M., Ricci-Tersenghi, F., Weigt, M., & Zecchina, R. (2002). Hiding solutions in random satisfiability problems: A statistical mechanics approach.Physical Review Letters,88(18), 188701.
[8] Boggs, P. T., & Tolle, J. W. (1995). Sequential quadratic programming.Acta numerica,4, 1-51. · Zbl 0828.65060
[9] Bradley, T., Faber, S., & Tsudik, G. (2016). Bounded size-hiding private set intersection. InInternational Conference on Security and Cryptography for Networks, pp. 449-467. · Zbl 1482.94043
[10] Bringer, J., & Chabanne, H. (2010). Negative databases for biometric data. InProceedings of the 12th ACM Workshop on Multimedia and Security, pp. 55-62.
[11] Dasgupta, D., & Azeem, R. (2008). An investigation of negative authentication systems. In Proceedings of 3rd international conference on information warfare and security, pp. 117-126.
[12] Dasgupta, D., & Saha, S. (2009).A biologically inspired password authentication system. InProceedings of the 5th Annual Workshop on Cyber Security and Information Intelligence Research: Cyber Security and Information Intelligence Challenges and Strategies, pp. 41-44.
[13] Esponda, F. (2008a). Everything that is not important: Negative databases.IEEE Computational Intelligence Magazine,3(2), 60-63.
[14] Esponda, F. (2008b). Hiding a needle in a haystack using negative databases. InInternational Workshop on Information Hiding, pp. 15-29.
[15] Esponda, F., Ackley, E. S., Forrest, S., & Helman, P. (2004). Online negative database. In Proceedings of the Third International Conference on Artificial Immune Systems, pp. 175-188.
[16] Esponda, F., Ackley, E. S., Helman, P., Jia, H., & Forrest, S. (2007). Protecting data privacy through hard-to-reverse negative databases.International Journal of Information Security,6(6), 403-415.
[17] Esponda, F., Forrest, S., & Helman, P. (2004). Enhancing privacy through negative representations of data.University of New Mexico, TR-CS-2004-18,50, 193.
[18] Esponda, F., Forrest, S., & Helman, P. (2009). Negative representations of information. International Journal of Information Security,8(5), 331-345.
[19] Fleury, A. B. K. F. M., & Heisinger, M. (2020). Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020.SAT COMPETITION,50, 2020.
[20] Gir´aldez-Cru, J., & Levy, J. (2016). Generating sat instances with community structure. Artificial Intelligence,238, 119-134. · Zbl 1385.68041
[21] Gir´aldez-Cru, J., & Levy, J. (2021). Popularity-similarity random sat formulas.Artificial Intelligence,299, 103537. · Zbl 1520.68104
[22] Gir´aldez-Cru, J., & Levy, J. (2017). Locality in random sat instances. InInternational Joint Conferences on Artificial Intelligence, p. 638-644.
[23] Jia, H., Moore, C., & Strain, D. (2007). Generating hard satisfiable formulas by hiding solutions deceptively.Journal of Artificial Intelligence Research,28, 107-118. · Zbl 1182.68249
[24] Lindell, Y., Nissim, K., & Orlandi, C. (2013). Hiding the input-size in secure two-party computation. InInternational Conference on the Theory and Application of Cryptology and Information Security 2013, pp. 421-440. · Zbl 1326.94110
[25] Liu, R., Luo, W., & Yue, L. (2014). The p-hidden algorithm: Hiding single databases more deeply.International Journal of Immune Computation,2(1), 43-55.
[26] Liu, R., Luo, W., & Yue, L. (2015). Hiding multiple solutions in a hard 3-SAT formula. Data & Knowledge Engineering,100, Part A, 1-18.
[27] Luo, W., Hu, Y., Jiang, H., & Wang, J. (2019). Authentication by encrypted negative password.IEEE Transactions on Information Forensics and Security,In press, DOI: 10.1109/TIFS.2018.2844854.
[28] Luo, W., Liu, R., Jiang, H., Zhao, D., & Wu, L. (2018). Three branches of negative representation of information: A survey.IEEE Transactions on Emerging Topics in Computational Intelligence,2(6), 411-425.
[29] Omelchenko, O., & Bulatov, A. (2021). Satisfiability and algorithms for non-uniform random k-SAT. InProceedings of the AAAI Conference on Artificial Intelligence, Vol. 35, pp. 3886-3894.
[30] SAT Competition (2016).Call for benchmarks. URL: https://baldur. iti.kit.edu/satcompetition-2016/index.php?cat=benchmarks..
[31] Selman, B., Kautz, H. A., Cohen, B., et al. (1995). Local search strategies for satisfiability testing.DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 26, 521-532.
[32] Selman, B., Mitchell, D. G., & Levesque, H. J. (1996). Generating hard satisfiability problems.Artificial Intelligence,81(1-2), 17-29. · Zbl 1508.68347
[33] Xu, K., Boussemart, F., Hemery, F., & Lecoutre, C. (2007). Random constraint satisfaction: Easy generation of hard (satisfiable) instances.Artificial Intelligence,171(8-9), 514- 534. · Zbl 1168.68554
[34] Xu, K., & Li, W. (2000). Exact phase transitions in random constraint satisfaction problems. Journal of Artificial Intelligence Research,12, 93-103. · Zbl 0940.68099
[35] Xu, K., & Li, W. (2006). Many hard examples in exact phase transitions.Theoretical Computer Science,355(3), 291-302. · Zbl 1088.68163
[36] Zhao, D., & Luo, W. (2013). A study of the private set intersection protocol based on negative databases. InProceedings of the 11th IEEE International Conference on Dependable, Autonomic and Secure Computing, pp. 58-64.
[37] Zhao, D., Luo, W., Liu, R., & Yue, L. (2015a). A fine-grained algorithm for generating hardto-reverse negative databases. InProceedings of the 2015 International Workshop on Artificial Immune Systems, pp. 1-8.
[38] Zhao, D., Luo, W., Liu, R., & Yue, L. (2015b). Negative iris recognition.IEEE Transactions on Dependable and Secure Computing,15(1), 112-125.
[39] Zhao, D., Luo, W., Liu, R., & Yue, L. (2017). Experimental analyses of the K-hidden algorithm.Engineering Applications of Artificial Intelligence,62, 331-340
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.