Clause-connected versions of the satisfiability problem

V. Yu. Popov

Sibirskie èlektronnye matematičeskie izvestiâ, Tome 21 (2024) no. 1, pp. 417-452

Résumé

The satisfiability problem is one of the most famous computationally hard algorithmic problems. It is well known that the satisfiability problem remains hard even in the restricted version in which Boolean formulas in conjunctive normal form with exactly three distinct literals per clause. However, the problem can be solved in polynomial time for Boolean formulas with exactly two distinct literals per clause. Narrowing the gap between the problems is of fundamental interest. Therefore, it is natural to analyze the complexity of some restricted versions of the satisfiability problem. In this paper, we prove hardness of some clause-connected versions of the satisfiability problem.

Détail

Keywords: satisfiability problem, computational complexity, NP-complete.

Bibliographie

[1] P. Berman, M. Karpinski, A.D. Scott, “Computational complexity of some restricted instances of 3-SAT”, Discrete Appl. Math., 155:5 (2007), 649–653 | DOI | MR | Zbl

[2] A. Darmann, J. Döcker, “On simplified NP-complete variants of Monotone 3-Sat”, Discrete Appl. Math., 292 (2021), 45–58 | DOI | MR | Zbl

[3] N. Misra, N.S. Narayanaswamy, V. Raman, B.S. Shankar, “Solving minones-2-sat as fast as vertex cover”, Mathematical foundations of computer science 2010, 35th international symposium, MFCS 2010, Proceedings (Brno, Czech Republic, August 23-27, 2010), Lecture Notes in Computer Science, 6281, eds. Hliněný, Petr et al., Springer, Berlin, 2010, 549–555 | DOI | MR | Zbl

[4] G.S. Tseitin, “On the complexity of derivation in propositional calculus”, Automation of Reasoning, Symbolic Computation, 1064, eds. Siekmann, J.H., Wrightson, G., Springer, Berlin–Heidelberg, 1983, 466–483 | DOI | MR

[5] A. Curtis, T. Silver, J.B. Tenenbaum, T. Lozano-Pérez, L. Kaelbling, “Discovering state and action abstractions for generalized task and motion planning”, Proceedings of the AAAI Conference on Artificial Intelligence, 36 (2022), 5377–5384 | DOI

[6] E. Ablad, D. Spensien, R. Bohlin, J.S. Carlson, A.-B. Strömberg, “Spatial-temporal load balancing and coordination of multi-robot stations”, IEEE Transactions on Automation Science and Engineering, 20:4 (2023), 2203–2214 | DOI

[7] D. Meli, H. Nakawala, P. Fiorini, “Logic programming for deliberative robotic task planning”, Artif. Intell. Rev., 56 (2023), 9011–9049 | DOI

[8] L. Matlekovic, P. Schneider-Kamp, “Constraint programming approach to coverage-path planning for autonomous multi-UAV infrastructure inspection”, Drones, 7:9 (2023), 563 | DOI

[9] L. Wang, W. Ma, L. Wang, Y. Ren, C. Yu, “Enabling in-depot automated routing and recharging scheduling for automated electric bus transit systems”, J. Advanced Transportation, 2021 (2021), 5531063 | DOI

[10] S. Abed, A. Ashkanan, W. Mansoor, A. Gawanmeh, “Enhanced SAT solvers based hashing method for bitcoin mining”, 17th International Conference on Information Technology-New Generations (ITNG 2020), Advances in Intelligent Systems and Computing, 1134, ed. Latifi, S., Springer, Cham, 2020, 191–198 | DOI

[11] M. Trimoska, S. Ionica, G. Dequen, “A SAT-based approach for index calculus on binary elliptic curves”, Progress in cryptology–AFRICACRYPT 2020, Lect. Notes Comput. Sci., 12174, eds. Nitaj, Abderrahmane et al., Springer, Cham, 2020, 214–235 | DOI | MR | Zbl

[12] S. Utsumi, K. Sakamoto, T. Isobe, “Bit-level evaluation of piccolo block cipher by satisfiability problem solver”, IET Information Security, 17:4 (2023), 616–625 | DOI

[13] C. Huang, M. Newman, M. Szegedy, “Explicit lower bounds on strong quantum simulation”, IEEE Trans. Inf. Theory, 66:9 (2020), 5585–5600 | DOI | MR | Zbl

[14] S. Schneider, L. Burgholzer, R. Wille, “A SAT encoding for optimal Clifford circuit synthesis”, Proceedings of the 28th Asia and South Pacific Design Automation Conference, 2023, 190–195 | DOI

[15] I. Bliznets, D. Sagunov, K. Simonov, “Fine-grained complexity of partial minimum satisfiability”, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022, 1774–1780 https://www.ijcai.org/proceedings/2022/0247.pdf

[16] Y. Lin, M. Althoff, “Rule-compliant trajectory repairing using satisfiability modulo theories”, IEEE Intelligent Vehicles Symposium, 4 (2022), 1–8 | DOI

[17] D. Caballero, T. Gomez, R. Schweller, T. Wylie, “Unique assembly verification in two-handed self-assembly”, Algorithmica, 85:8 (2023), 2427–2453 | DOI | MR | Zbl

[18] E.D. Demaine, S. Eisenstat, “Flattening fixed-angle chains is strongly NP-hard”, Algorithms and data structures, 12th international symposium, WADS 2011, Proceedings, Lecture Notes in Computer Science, 6844, eds. Dehne, Frank et al., Springer, Berlin, 2011, 314–325 | DOI | MR | Zbl

[19] F. Imeson, S.L. Smith, “An SMT-based approach to motion planning for multiple robots with complex constraints”, IEEE Transactions on Robotics, 35:3 (2019), 669–684 | DOI

[20] J. Giráldez-Cru, J. Levy, “Generating SAT instances with community structure”, Artif. Intell., 238 (2016), 119–134 | DOI | MR | Zbl

[21] G. Amendola, F. Ricca, M. Truszczynski, “New models for generating hard random Boolean formulas and disjunctive logic programs”, Artif. Intell., 279 (2020), 103185 | DOI | MR | Zbl

[22] D. Barak-Pelleg, D. Berend, J.C. Saunders, “A model of random industrial SAT”, Theor. Comput. Sci., 910 (2022), 91–112 | DOI | MR | Zbl

[23] R. Heradio, D. Fernandez-Amoros, J. A. Galindo, D. Benavides, D. Batory, “Uniform and scalable sampling of highly configurable systems”, Empir. Software Eng., 27 (2022), 44 | DOI

[24] C. Ebert, M. Weyrich, B. Lindemann, S.P. Chandrasekar, “Systematic testing for autonomous driving”, ATZelectronics worldwide, 16 (2021), 18–23 | DOI

[25] W. Guo, H.-L. Zhen, X. Li, W. Luo, M. Yuan, Y. Jin, J. Yan, “Machine learning methods in solving the boolean satisfiability problem”, Mach. Intell. Res., 20 (2023), 640–655 | DOI

[26] L. Sun, D. Gerault, A. Benamira, T. Peyrin, “NeuroGIFT: Using a machine learning based sat folver for cryptanalysis”, Cyber Security Cryptography and Machine Learning, CSCML 2020, Lecture Notes in Computer Science, 12161, eds. Dolev, S., Kolesnikov, V., Lodha, S., Weiss, G., Springer, Cham, 2020, 62–84 | DOI | MR

[27] A.M. Leventi-Peetz, J.-V. Peetz, M. Rohde, “ML Supported predictions for SAT solvers performance”, Proceedings of the Future Technologies Conference (FTC) 2019, FTC 2019, Advances in Intelligent Systems and Computing, 1069, eds. Arai, K., Bhatia, R., Kapoor, S., Springer, Cham, 2019, 64–78 | DOI

[28] M. Mosca, S. R.Verschoor, “Factoring semi-primes with (quantum) SAT-solvers”, Sci. Rep., 12 (2022), 7982 | DOI

[29] P. Branco, P. Mateus, C. Salema, A. Souto, “Using low-density parity-check codes to improve the McEliece cryptosystem”, Inf. Sci., 510 (2020), 243–255 | DOI | MR | Zbl

[30] M. Egger, M. Xhemrishi, A. Wachter-Zeh, R. Bitar, “Sparse and private distributed matrix multiplication with straggler tolerance”, IEEE International Symposium on Information Theory (Taipei), IEEE, 2023 | DOI | MR

[31] P. Pérez-Pacheco, P. Caballero-Gil, “McEliece cryptosystem: Reducing the key size with QC-LDPC codes”, 19th International Conference on the Design of Reliable Communication Networks (Vilanova i la Geltru), IEEE, 2023 | DOI

[32] S. Afzal, M. Yousaf, H. Afzal, N. Alharbe, M. R. Mufti, “Cryptographic strength evaluation of key schedule algorithms”, Security and Communication Networks, 2020 (2020), 3189601 | DOI

[33] M. Baldi, J.-C. Deneuville, E. Persichetti, P. Santini, “Cryptanalysis of a code-based signature scheme based on the Schnorr-Lyubashevsky framework”, IEEE Communications Letters, 25:9 (2021), 2829–2833 | DOI | MR

[34] A.K. Hartmann, M. Weigt, Phase transitions in combinatorial optimization problems. Basics, algorithms and statistical mechanics, WILEY-VCH, Weinheim, 2005 | DOI | MR | Zbl

[35] M. Mézard, A. Montanari, Information, physics and computation, Oxford University Press, Oxford, 2009 | DOI | MR | Zbl

[36] C. Moore, S. Mertens, The nature of computation, Oxford University Press, Oxford, 2011 | DOI | MR | Zbl

[37] D. Mitchell, B. Selman, H. Levesque, “Hard and easy distributions of SAT problems”, Proceedings of the 10th National Conference on Artificial Intelligence, AAAI, 1992, 459–465 https://cdn.aaai.org/AAAI/1992/AAAI92-071.pdf

[38] P. Cheeseman, B. Kanefsky, W.M. Taylor, “Where the really hard problems are”, Artificial intelligence, IJCAI-91, Proc. 12th Int. Conf. (Sydney/Australia, 1991), 1991, 331–337 https://www.dcs.gla.ac.uk/p̃at/cpM/papers/cheeseman91where.pdf | Zbl

[39] J. Sleegers, R. Olij, G. van Horn, D. van den Berg, “Where the really hard problems aren't”, Operations Research Perspectives, 7 (2000), 100160 | DOI | MR

[40] M. Mézard, G. Parisi, R. Zecchina, “Analytic and algorithmic solution of random satisfiability problems”, Science, 297:5582 (2002), 812–815 | DOI

[41] G. Biroli, S. Cocco, R. Monasson, “Phase transitions and complexity in computer science: An overview of the statistical physics approach to the random satisfiability problem”, Physica A, 306 (2002), 381–394 | DOI | Zbl

[42] W. Perkins, Searching for (sharp) thresholds in random structures: where are we now?, 2024, arXiv: 2401.01800 | DOI | MR

[43] J. Ding, A. Sly, N. Sun, “Satisfiability threshold for random regular NAE-SAT”, Commun. Math. Phys., 341:2 (2016), 435–489 | DOI | MR | Zbl

[44] J. Ding, A. Sly, N. Sun, “Proof of the satisfiability conjecture for large k”, Ann. Math. (2), 196:1 (2022), 1–388 | DOI | MR | Zbl

[45] J. Park, H.T. Pham, “A proof of the Kahn-Kalai conjecture”, J. Am. Math. Soc., 37:1 (2024), 235–243 | DOI | MR | Zbl

[46] H. Schawe, R. Bleim, A. K. Hartmann, “Phase transitions of the typical algorithmic complexity of the random satisfiability problem studied with linear programming”, PLoS One, 14 (2019), e0215309 | DOI

[47] S.E. Schmittner, A SAT-based public key cryptography scheme, 2015, arXiv: 1507.08094v3 | DOI | MR

[48] R. Sun, Q. Peng, Y. Tian, “A hybrid encryption scheme based on the satisfiability problem”, IEEE Global Conference on Signal and Information Processing (Montreal), IEEE, 2017, 1363–1367 | DOI

[49] J. Thomas, N.S. Chaudhari, “Hybrid cryptosystem based on 2-SAT 3-SAT and the implications of polynomial solvability of 3-SAT”, International J. Comp. Appl., 2 (2011), 1–6 https://research.ijcaonline.org/encc/number2/encc009.pdf

[50] Y. Li, X. Chen, W. Guo, X. Li, W. Luo, J. Huang, H.-L. Zhen, M. Yuan, J. Yan, “HardSATGEN: Understanding the difficulty of hard SAT formula generation and a strong structure-hardness-aware baseline”, Proceedings of the 29th ACM SIGKDD Conference on Knowledge Discovery and Data Mining, 2023, 4414–4425 | DOI

[51] Z. Newsham, V. Ganesh, S. Fischmeister, G. Audemard, L. Simon, “Impact of community structure on SAT solver performance”, Theory and applications of satisfiability testing - SAT 2014, 17th international conference, Proceedings, Lect. Notes Comput. Sci., 8561, eds. Sinz, Carsten et al., Springer, Berlin, 2014, 252–268 | DOI | MR | Zbl

[52] A. Slater, “Modelling more realistic SAT problems”, AI 2002: Advances in artificial intelligence, 15th Australian joint conference on artificial intelligence, Proceedings (Canberra, Australia, December 2-6, 2002), Lecture Notes in Computer Science, 2557, eds. McKay, Bob et al., 2002, 591–602 | DOI | MR | Zbl

[53] E.D. Demaine, K. Karntikoon, N. Pitimanaaree, 2-colorable perfect matching is NP-complete in 2-connected 3-regular planar graphs, 2023, arXiv: 2309.09786v1 | MR

[54] S.A. Cook, “The complexity of theorem-proving procedures”, Proc. 3rd ann. ACM Sympos. Theory Computing (Shaker Heights, Ohio), ACM, 1971, 151–158 | DOI | Zbl

[55] M.R. Garey, D.S. Johnson, Computers and intractability. A guide to the theory of NP-completeness, W.H. Freeman and Company, San Francisco, 1979 https://djvu.online/file/sEtkhOgJV2w9w | Zbl

[56] R.M. Karp, “Reducibility among combinatorial problems”, Complexity of computer computations, Proceedings of a symposium on the complexity of computer computations, The IBM Research Symposia Series, eds. Miller, Raymond E. et al., Plenum Press, New York-London, 1972, 85–103 | DOI | MR | Zbl

[57] L. Juban, “Dichotomy theorem for the generalized unique satisfiability problem”, Fundamentals of computation theory, 12th international symposium, FCT '99, Proceedings (Iaşi, Romania, August 30–September 3, 1999), Lect. Notes Comput. Sci., 1684, eds. Ciobanu, Gabriel et al., Springer, Berlin, 1999, 327–337 | DOI | MR | Zbl

[58] C. Sundermann, T. Heß, M. Nieke, P. Bittner, J. Young, T. Thüm, I. Schaefer, “Evaluating state-of-the-art # SAT solvers on industrial configuration spaces”, Empir. Software Eng., 28 (2023), 29 | DOI

[59] C. Sundermann, T. Thüm, I. Schaefer, “Evaluating #SAT solvers on industrial feature models”, Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems, 2020, 3 | DOI

[60] D. Zhao, L. Liao, W. Luo, J. Xiang, H. Jiang, X. Hu, “Generating random SAT instances: multiple solutions could be predefined and deeply hidden”, J. Artif. Intell. Res. (JAIR), 76 (2023), 435–470 | DOI | MR | Zbl

[61] R.G. Downey, M.R. Fellows, Parameterized complexity, Springer, Berlin, 1999 | DOI | MR | Zbl

[62] J. Flum, M. Grohe, “The parameterized complexity of counting problems”, SIAM J. Comput., 33:4 (2004), 8921–922 | DOI | MR | Zbl

[63] R.E. Ladner, N.A. Lynch, A.L. Selman, “A comparison of polynomial time reducibilities”, Theor. Comput. Sci., 1 (1975), 103–123 | DOI | MR | Zbl

[64] C.H. Papadimitriou, Computational complexity, Addison-Wesley, Amsterdam, 1994 | MR | Zbl

[65] A. Jayasena, P. Mishra, “Directed test generation for hardware validation: A survey”, ACM Comput. Surv., 56:5 (2024), 132 | DOI | MR

[66] F. Lin, Y. Zhao, “ASSAT: computing answer sets of a logic program by SAT solvers”, Artif. Intell., 157:1-2 (2004), 115–137 | DOI | MR | Zbl

[67] A. Rubio, R. Cantarero, A. Margara, G. Cugola, D. Villa, J.C. López, “Commonsense reasoning and automatic generation of IoT contextual knowledge: An answer set programming approach”, Internet of Things, 25 (2024), 100998 | DOI

[68] T. Soh, N. Tamura, M. Banbara, “Scarab: A rapid prototyping tool for SAT-based constraint programming systems”, Lecture Notes in Computer Science, 7962, Springer, Berlin–Heidelberg, 2013, 429–436 | DOI

[69] D. Kim, N.M. Rahman, S. Mukhopadhyay, “PRESTO: A processing-in-memory-based k-SAT solver using recurrent stochastic neural network with unsupervised learning”, IEEE J. Solid-State Circuits, 2024, 1–11 | DOI

[70] A.A. Sohanghpurwala, M.W. Hassan, P. Athanas, “Hardware accelerated SAT solvers –A survey”, J. Parallel Distributed Computing, 106 (2017), 170–184 | DOI

[71] W. Hu, L. Zhang, A. Ardeshiricham, J. Blackstone, B. Hou, Y. Tai, R. Kastner, “Why you should care about don't cares: Exploiting internal don't care conditions for hardware Trojans”, IEEE/ACM International Conference on Computer-Aided Design (Irvine), IEEE, 2017, 707–713 | DOI

[72] D.G. Mahmoud, B. Shokry, V. Lenders, W. Hu, M. Stojilović, “X-attack 2.0: The risk of power wasters and satisfiability don't-care hardware trojans to shared cloud FPGAs”, IEEE Access, 12 (2024), 8983–9011 | DOI

[73] Y. Su, T.T.-H. Kim, B. Kim, “FlexSpin: A CMOS ising machine with 256 flexible spin processing elements with 8-b coefficients for solving combinatorial optimization problems”, IEEE Journal of Solid-State Circuits, 2024, 1–12 | DOI

[74] H. Spakowski, M. Thakur, R. Tripathi, “Quantum and classical complexity classes: Separations, collapses, and closure properties”, Inf. Computat., 200:1 (2005), 1–34 | DOI | MR | Zbl

[75] M. Ogiwara, L. A. Hemachandra, “A complexity theory for feasible closure properties”, J. Comput. Syst. Sci., 46:3 (1993), 295–325 | DOI | MR | Zbl

[76] J. Gill, “Computational complexity of probabilistic Turing machines”, SIAM J. Comput., 6 (1977), 675–695 | DOI | MR | Zbl

[77] J. Simon, On some central problems in computational complexity, Cornell Department of Computer Science Technical Report TR75-224, PhD thesis, Cornell University, Ithaca, 1975 https://hdl.handle.net/1813/6975

[78] R. Beigel, J. Gill, “Counting classes: Thresholds, parity, mods, and fewness”, Theor. Comput. Sci., 103:1 (1992), 3–23 | DOI | MR | Zbl

[79] J. Cai, L. Hemachandra, “On the power of parity polynomial time”, Math. Syst. Theory, 23:2 (1990), 95–106 | DOI | MR | Zbl

[80] U. Hertrampf, “Relations among MOD-classes”, Theor. Comput. Sci., 74:3 (1990), 325–328 | DOI | MR | Zbl

[81] L. Goldschlager, I. Parberry, “On the construction of parallel computers from various bases of Boolean functions”, Theor. Comput. Sci., 43 (1986), 43–58 | DOI | MR | Zbl

[82] C. Papadimitriou, S. Zachos, “Two remarks on the power of counting”, Theoretical computer science, 6th GI-Conf. (Dortmund 1983), Lect. Notes Comput. Sci., 145, 1983, 269–276 | DOI | Zbl

[83] S. Fenner, L. Fortnow, S. Kurtz, “Gap-definable counting classes”, J. Comput. Syst. Sci., 48:1 (1994), 116–148 | DOI | MR | Zbl

[84] K.W. Wagner, “The complexity of combinatorial problems with succinct input representations”, Acta Inf., 23 (1986), 325–356 | DOI | MR | Zbl

[85] R.P.N. Rao, J. Rothe, O. Watanabe, “Upward separation for FewP and related classes”, Inf. Process. Lett., 52:4 (1994), 175–180 | DOI | MR | Zbl

[86] L.G. Valiant, “The complexity of computing the permanent”, Theor. Comput. Sci., 8 (1979), 189–201 | DOI | MR | Zbl

[87] R. Barbanchon, “On unique graph 3-colorability and parsimonious reductions in the plane”, Theor. Comput. Sci., 319:1-3 (2004), 455–482 | DOI | MR | Zbl

[88] E. Bakali, A. Chalki, S. Kanellopoulos, A. Pagourtzis, S. Zachos, On the power of counting the total number of computation paths of NPTMs, 2024, arXiv: 2306.11614v3 | DOI | MR

[89] D. Lichtenstein, “Planar formulae and their uses”, SIAM J. Comput., 11 (1982), 329–343 | DOI | MR | Zbl

[90] B.M.E. Moret, “Planar NAE3SAT is in P”, SIGACT News, 19:2 (1988), 51–54 | DOI | MR | Zbl

[91] M.E. Dyer, A.M. Frieze, “Planar 3DM is NP-complete”, J. Algorithms, 7 (1986), 174–184 | DOI | MR | Zbl

[92] H.B. Hunt III, M.V. Marathe, V. Radhakrishnan, R.E. Stearns, “The complexity of planar counting problems”, SIAM J. Comput., 27:4 (1998), 1142–1167 | DOI | MR | Zbl

[93] O. Goldreich, Computational complexity. A conceptual perspective, Cambridge University Press, Cambridge, 2008 | DOI | MR | Zbl

[94] E. Friedgut, J. Bourgain, “Sharp thresholds of graph properties, and the k-SAT problem”, J. Am. Math. Soc., 12:4 (1999), 1017–1054 | DOI | MR | Zbl

[95] V. Chvátal, B. Reed, “Mick gets some (the odds are on his side)”, Proceedings of the 33rd Annual Symposium on Foundations of Computer Science, IEEE Computer Society Press, Washington, 1992, 620–627 | DOI | Zbl

[96] A. Goerdt, “A threshold for unsatisfiability”, Mathematical foundations of computer science 1992, 17th international symposium, Proceedings (August 24-28, 1992, Prague, Czechoslovakia), Lect. Notes Comput. Sci., 629, eds. Havel, Ivan M. et al., Springer, Berlin, 1992, 264–274 | DOI | MR | Zbl

[97] A. Goerdt, “A threshold for unsatisfiability”, J. Comput. Syst. Sci., 53:3 (1996), 469–486 | DOI | MR | Zbl

[98] B. Bollobás, C. Borgs, J.T. Chayes, J.H. Kim, D.B. Wilson, “The scaling window of the 2-SAT transition”, Random Struct. Algorithms, 18:3 (2001), 201–256 | DOI | MR | Zbl

[99] J.M. Crawford, L.D. Auton, “Experimental results on the crossover point in random 3-SAT”, Artif. Intell., 81:1-2 (1996), 31–57 | DOI | MR | Zbl

[100] O. Dubois, Y. Boufkhad, J. Mandler, “Typical random 3-SAT formulae and the satisfiability threshold”, Proceedings of the 11th annual ACM-SIAM symposium on Discrete algorithms (Philadelphia), SIAM, San Francisco, 2000, 126–127 | DOI | Zbl

[101] A.C. Kaporis, L.M. Kirousis, E.G. Lalas, “The probabilistic analysis of a greedy satisfiability algorithm”, Random Struct. Algorithms, 28:4 (2006), 444–480 | DOI | MR | Zbl

[102] M. Mézard, “Optimization and physics: On the satisfiability of random boolean Formulae”, International Conference on Theoretical Physics, Birkhäuser, Basel, 2003, 475–488 | DOI | MR

[103] J. Franco, “Typical case complexity of satisfiability algorithms and the threshold phenomenon”, Discrete Appl. Math., 153:1-3 (2005), 89–123 | DOI | MR | Zbl

[104] H. Fu, S. Cai, G. Wu, J. Liu, X. Yang, Y. Xu, “Improving two-mode algorithm via probabilistic selection for solving satisfiability problem”, Information Sci., 653 (2024), 119751 | DOI

[105] H. Fu, Y. Xu, G. Wu, J. Liu, S. Chen, X. He, “Emphasis on the flipping variable: Towards effective local search for hard random satisfiability”, Information Sci., 566 (2021), 118–139 | DOI | MR

[106] T.N. Alyahya, M.E.B. Menai, H. Mathkour, “On the structure of the Boolean satisfiability problem: A survey”, ACM Comput. Surveys, 55:3 (2022), 46 | DOI

[107] T. Al-Yahya, M.E.B.A. Menai, H. Mathkour, “Boosting the performance of CDCL-based SAT solvers by exploiting backbones and backdoors”, Algorithms, 15:9 (2022), 302 | DOI

[108] Z. Zhang, D. Xu, J. Zhou, “An algorithm for solving satisfiability problem based on the structural information of formulas”, Front. Comput. Sci., 15 (2021), 156405 | DOI

[109] M.A.H. Newton, M.M.A. Polash, D N. Pham, J. Thornton, K. Su, A. Sattar, “Evaluating logic gate constraints in local search for structured satisfiability problems”, Artif. Intell. Rev., 54 (2021), 5347–5411 | DOI

[110] R. Ostrowski, É. Grégoire, B. Mazure, L Saïs, “Recovering and exploiting structural knowledge from CNF formulas”, Principles and Practice of Constraint Programming-CP 2002. CP 2002, Lecture Notes in Computer Science, 2470, eds. Van Hentenryck, P., Springer, Berlin, 2002, 185–199 | DOI

[111] D.A. Plaisted, S. Greenbaum, “A structure-preserving clause form translation”, J. Symb. Comput., 2 (1986), 293–304 | DOI | MR | Zbl

[112] S.R.B. Bearden, Y.R. Pei, M. Di Ventra, “Efficient solution of Boolean satisfiability problems with digital memcomputing”, Sci. Reports, 10 (2020), 19741 | DOI

[113] S. Cai, C. Luo, K. Su, “Improving walkSAT by effective Tie-breaking and efficient implementation”, The Computer Journal, 58:11 (2015), 2864–2875 | DOI

[114] H. Fu, Y. Xu, S. Chen, J. Liu, “Improving walkSAT for random 3-SAT problems”, J. Univ. Comput. Sci., 26:2 (2020), 220–243 | DOI | MR