<p>The critical nodes detection problem (CNDP) involves identifying a limited number of nodes for removal from an undirected graph, to maximize the disconnections between remaining node pairs. In this paper, we shall provide a high-efficiency algorithm for precisely solving the integer programming (IP) formulations for the CNDP. Firstly, a preprocessing procedure is introduced, which can not only reduce the size of the exponential-size IP formulation of the problem but also strengthen the linear programming relaxation. Secondly, the polyhedral properties of the polytope associated with the exponential-size IP formulation are explored, providing a flexible way to derive facet-defining inequalities for the polytope from certain projected ones. Thirdly, a family of strong valid inequalities based on clique subgraphs is developed for the polytope, with both necessary and sufficient conditions for them to be facet-defining. The complexity and algorithm of the separation problem for these inequalities are also investigated. Finally, we extend our research findings from the exponential-size IP formulation to two polynomial-size IP reformulations for the CNDP. Computational results demonstrate the efficacy of incorporating our proposed preprocessing and valid inequalities into an IP solver for solving all three CNDP formulations.</p>