The use of backdoors to estimate the hardness of propositional proofs and cryptographic attacks

A. A. Semenov

Prikladnaya Diskretnaya Matematika. Supplement, no. 16 (2023), pp. 87-95.

Résumé

In the paper, we consider the problem of constructing tree-like unsatisfiability proof certificates under the assumption that this proof is generated by a SAT solver based on the CDCL algorithm. Such tree-like representations are convenient when it is necessary to evaluate how hard it is to prove the unsatisfiability of a specific formula, or to estimate the runtime of some cryptographic attack mounted using the SAT solver. We propose tree-like descriptions of CDCL scenarios in application to both unsatisfiable formulas arising in, e.g. symbolic verification, and to satisfiable formulas encoding the problems of inversion of discrete functions (including cryptographic ones). We prove a number of properties of the introduced tree-like structures. In particular, we formulate the basic property of the class of cryptographic attacks based on inverse backdoor sets in the language of the proposed structures.

Détail

Keywords: Boolean satisfiability $($SAT$)$, propositional proof system, backdoor, CDCL algorithm.

Bibliographie

[1] Robinson J. A., “Machine-oriented logic based on resolution principle”, J. ACM, 12:1 (1965), 23–41 | DOI | MR | Zbl

[2] Davis M., Logemann G., and Loveland D., “A machine program for theorem-proving”, Commun. ACM, 5:7 (1962), 394–397 | DOI | MR | Zbl

[3] Marques-Silva J. and Sakallah K., “GRASP: A new search algorithm for satisfiability”, Proc. ICCAD (San Jose, CA, USA, 1996), 220–227

[4] Cook S. and Reckhow R., “The relative efficiency of propositional proof systems”, J. Symbolic Logic, 44:1 (1979), 36–50 | DOI | MR | Zbl

[5] Ben-Sasson E. and Wigderson A., “Short proofs are narrow — resolution made simple”, J. ACM, 48:2 (2001), 149–169 | DOI | MR | Zbl

[6] Bonet M. L., Esteban J. L., Galesi N., and Johannsen J., “Exponential separations between restricted resolution and cutting planes proof systems”, Proc. 39th Ann. Symp. FOCS (Palo Alto, CA, USA, 1998), 638–647

[7] Beame P. and Pitassi T., “Simplified and improved resolution lower bounds”, Proc. 37th Conf. FOCS (Burlington, VT, USA, 1996), 274–282 | MR

[8] Ansotegui C., Bonet M. L., Levy J., and Manya F., “Measuring the hardness of SAT instances”, Proc. AAAI Conf. (Chicago, Illinois, USA, July 13–17, 2008), 222–228

[9] Williams R., Gomes C., and Selman B., “Backdoors to typical case complexity”, Proc. 18th Int. Conf. IJCAI (Acapulco, Mexico, 2003), 1173–1178

[10] Semenov A., Chivilikhin D., Pavlenko A., et al., “Evaluating the hardness of SAT instances using evolutionary algorithms”, Proc. 27th Int. Conf. CP 2021, 47, 1–18 | MR

[11] Semenov A., Zaikin O., Otpuschennikov I., et al., “On cryptographic attacks using backdoors for SAT”, Proc. AAAI (New Orleans, Louisiana, USA, 2018), 6641–6648

[12] Marques-Silva J., Lynce I., and Malik S., “Conflict-driven clause learning SAT solvers”, Handbook of Satisfiability, Second Ed., IOS Press, 2021, 133–182

[13] Molitor P. and Mohnke J., Equivalence Checking of Digital Circuits: Fundamentals, Principles, Methods, Kluwer Academic Publ., 2004 | Zbl

[14] Tseitin G. S., “O slozhnosti vyvoda v ischislenii vyskazyvanii”, Zapiski nauchn. seminarov LOMI, 8, 1968, 234–259 | MR | Zbl

[15] Yablonskii S. V., Vvedenie v diskretnuyu matematiku, Nauka, M., 1986 | MR

[16] Chivilikhin D., Pavlenko A., and Semenov A., “Decomposing hard SAT instances with metaheuristic optimization”, Intern. J. Artificial Intelligence, 21:2 (2023), 61–92

[17] Goldreich O., Computational Complexity: A Conceptual Perspective, Cambridge University Press, 2008 | MR | Zbl

[18] Semenov A., Otpuschennikov I., Gribanova I., et al., “Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems”, Logical Methods in Computer Sci., 16:1 (2020), 29, 1–42 | MR

[19] Chang C. and Lee R., Symbolic Logic and Mechanical Theorem Proving, Elsevier, 1973 | MR