I am having a hard time to believe that the solver actually tries all solutions
Indeed, they typically do not explore the whole search space (though it's possible to build problematic instances where they would).
MILP solvers will use a combination of tools to do so, under the umbrella of the branch-and-cut paradigm (B&C is basically branch-and-bound with cutting planes).
In the rest of my answer I assume basic familiarity with branch-and-bound schemes.
First, presolve will typically reduce the size of the problem, by eliminating variables, fixing some, aggregating some constraints, finding symmetries, etc.
For instance, if your problem has a constraint of the form
$$
x + 3y \leq 2
$$
for $x, y$ binary, then you can already set $y$ to zero (otherwise the constraint is automatically violated).
Doing this kind of reductions can significantly reduce the search space.
The rest of the proof lies in the branch-and-bound tree.
Imagine a problem with $100$ binary variables, which would give an exploration tree of $2^{100}$ leaves.
A branch=and-bound algorithm will cut portions of that tree using various rules, thereby avoiding the need to explore it all.
There are mainly 2 ways of doing so:
- showing that a node in the tree (and thus all of its children) does not contain any feasible integer solution
- showing that a node in the tree (and thus all of its children) does not contain any optimal integer solution
Cutting planes
Cutting planes naturally restrict the search space.
Assume that, at the current node, a binary variable $x$ takes value $0.5$, and that you find a valid cut $x \leq 0.6$.
Then, you know that the branching decision $x =1$ will result in an infeasible problem: you can prune the corresponding node, and all of its children.
The earlier you can do so, the bigger the savings. This is why most of the cuts are typically generated at the root node of the tree.
Pruning by bound
Assume you have a feasible solution to your problem, and its objective value is $100$.
Now, assume that, at the current node, the linear relaxation has an objective value of $110$.
Then, any integer point (if any) that would be obtained from any of the current's node children, would have an objective value of at least $110$: none of them can be optimal, and you can discard the node.
Again, the earlier you can do that, the better.
Note that better linear relaxation provide better bounds, and there allow to discard nodes earlier, which speeds up performance.
Cutting planes also improve the linear relaxation, thereby providing tighter bounds, which also helps to prune nodes faster.
Other tricks
The two techniques outlines above are, as far as I know, the most generic & common ones to prove optimality in an MILP; though not the only ones.
Other techniques include:
- reduced-cost fixing, which allows one to prove that a variable $x$ must take a certain value in any integer-optimal solution
- symmetry detection, which allow to discard portions of the search tree by showing only a small part needs to be explored for correctness
- integrality of the objective: if all variables are integer, and all objective coefficients are integer, then the optimal value must be integer. So, if you have a solution with objective value $10$, and a lower bound of $9.5$, you know you have the optimal. Obviously this does not hold for the mixed-integer case.