Оценки трудности доказательств и криптографических атак, основанных на лазейках

Рассматривается задача построения древовидных сертификатов доказательств невыполнимости булевых формул в предположении, что такое доказательство генерируется SAT-решателем, основанным на алгоритме CDCL. Такого сорта древовидные представления удобны, когда для конкретной формулы требуется оценить, насколько трудно доказать её невыполнимость, либо требуется оценить трудоёмкость некоторой криптографической атаки, осуществляемой при помощи SAT-решателя. Предложены древовидные описания сценариев работы CDCL в применении как к невыполнимым формулам, возникающим, например, в задачах символьной верификации, так и к выполнимым формулам, кодирующим задачи обращения дискретных (в том числе криптографических) функций. Доказан ряд свойств введённых древовидных структур. В частности, на языке таких структур сформулировано базовое свойство класса криптографических атак, основанного на инверсных лазейках.