There are many of the formulations to linearize logical constraints by introducing new auxiliary binary or any appropriate variables and adding the corresponding constraints to the model. It can be found by a simple search on the community or other available resources on the web easily.
Now, I am interested to know how the standard MIP solvers do that automatically and how they found the suitable formulation. Once I tried a simple logical expression by CPLEX. By adding one or two binary variables and their related constraints the problem was solved.
But, when I tried the automatic mode by adding special if-then constraints and writing the model in the LP format, I saw there exist more than eight binary variables. I am looking for a standard method, but I cannot find any related resources.