An efficient Integer programming model for the minimum spanning tree problem?

Let $$T=(V, E')$$ be a spanning tree of a graph $$G=(V, E)$$. Rather than verifying for any subset of vertices $$S\subseteq V$$ that $$|E'(S)|=|S|-1$$, is there an efficient way to satisfy the spanning tree constraint (as the complexity for calculating all vertices subsets is exponential)?

To confirm that $$T$$ is a tree, you need to confirm that (a) it is connected and (b) $$\vert E'\vert = \vert V \vert - 1$$. The second part is trivial. To confirm it is connected, start at an arbitrarily chosen node $$v\in V$$ and label all nodes adjacent to $$v$$ in $$T$$. For each freshly labeled node, label all unlabeled nodes adjacent to it and proceed recursively until you run out of nodes to process. If all nodes ended up labeled, $$T$$ is connected, and you are done.