  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.
