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

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.