Front-end algorithm for solving the SAT problem

The algorithm for calculating the semantic value of conjunctive formulas of the form $U = F(X_1, X_2,..., X_n)$ in non-classical propositional logic $L_{S_{2}}$ also calculates the set of all solutions of the logical equation
$$F({x_1}, {x_2},..., {x_n})= 1.$$
Where $F(X_1, X_2,..., X_n)$ — a formula of Boolean algebra of the sets making a discrete Venn diagram. The elements of these sets are non-negative integers. Based on this algorithm, a new algorithm is built to solve the $ SAT~$ problem. A significant difference between it and a family of algorithms based on $ DPLL $ and $ CDCL $ is the replacement of Boolean variables with sets. This allows you to effectively check the feasibility of not one, but many sets of values of the logical variables ${x_1}, {x_2},..., {x_n}$.