In the article, within the framework of the Boolean Satisfiability problem (SAT), the problem of estimating the hardness of specific Boolean formulas w.r.t. a specific complete SAT solving algorithm is considered. Based on the well-known Strong Backdoor Set (SBS) concept, we introduce the notion of decomposition hardness (d-hardness). If $B$ is an arbitrary subset of the set of variables occurring in a SAT formula $C$, and $A$ is an arbitrary complete SAT solver , then the d-hardness expresses an estimate of the hardness of $C$ w.r.t. $A$ and $B$. We show that the d-hardness of $C$ w.r.t. a particular $B$ can be expressed in terms of the expected value of a special random variable associated with $A$, $B$, and $C$. For its computational evaluation, algorithms based on the Monte Carlo method can be used. The problem of finding $B$ with the minimum value of d-hardness is formulated as an optimization problem for a pseudo-Boolean function whose values are calculated as a result of a probabilistic experiment. To minimize this function, we use evolutionary algorithms. In the experimental part, we demonstrate the applicability of the concept of d-hardness and the methods of its estimation to solving hard unsatisfiable SAT instances.

翻译：在布尔可满足性问题（SAT）框架内，本文研究了特定布尔公式相对于特定完备SAT求解算法的困难度估计问题。基于著名的强后门集（Strong Backdoor Set, SBS）概念，我们引入了分解困难度（d-hardness）概念。若$B$是SAT公式$C$中变量集的任意子集，$A$为任意完备SAT求解器，则d-hardness表示$C$相对于$A$和$B$的困难度估计值。我们证明了$C$相对于特定$B$的d-hardness可表示为与$A$、$B$、$C$相关的特殊随机变量的期望值。其计算评估可采用基于蒙特卡洛方法的算法。寻找最小d-hardness值对应的$B$的问题被表述为伪布尔函数的优化问题，其函数值通过概率实验计算得出。为最小化该函数，我们采用进化算法。实验部分展示了d-hardness概念及其估计方法在求解困难不可满足SAT实例中的适用性。