Abstract: The paper proposes a probabilistic generalization of the well-known Strong Backdoor Set~(SBS) concept applied to the Boolean Satisfiability Problem (SAT).

We call a set of Boolean variables $B$ a $\rho$-backdoor, if for a fraction $\rho$ of possible assignments of variables from $B$, assigning their values to variables in a Boolean formula in Conjunctive Normal Form (CNF) results in polynomially solvable formulas.

Clearly, a $\rho$-backdoor with $\rho=1$ is an SBS.

For a given set $B$ it is possible to efficiently construct an $(\varepsilon, \delta)$-approximation of parameter $\rho$ using the Monte Carlo method.

Thus, we define an $(\varepsilon, \delta)$-SBS as such a set $B$ for which the estimation of the parameter $\rho$ deviates from 1 by no more than $\varepsilon$ with probability no less than $1-\delta$.

We consider the problems of finding the minimum SBS and the minimum $(\varepsilon, \delta)$-SBS.

To solve the former, one can use the algorithm described by R.~Williams, C.~Gomes and B.~Selman in 2003.

In the paper we propose a new probabilistic algorithm to solve the latter, and show that the asymptotic estimation of the worst case complexity of the proposed algorithm is significantly smaller than that of the algorithm by Williams~et~al.

For practical applications, we suggest a metaheuristic optimization algorithm based on the penalty function method to seek the minimal $(\varepsilon, \delta)$-SBS.

Results of computational experiments show that the use of $(\varepsilon, \delta)$-SBSes found by the proposed algorithm allows speeding up solving of test problems related to equivalence checking and hard crafted and combinatorial benchmarks compared to state-of-the-art SAT solvers.