SPFA判负环算法有两种主流判定方式，核心都基于图论的抽屉原理完成严谨证明：
前言：SPFA基于bellman-foyd，想不通就用bellman-foyd来想想
一、基于点入队次数的判定证明
- 判定规则：若图中某节点的入队次数≥总节点数n，则图中存在负环。
- 证明逻辑：
每次节点入队都对应一次最短路径的松弛更新，且更新后该点对应的最短路边数严格递增。当某点入队n次时，说明它对应的最短路径边数≥n，路径上的节点总数至少为n+1。根据抽屉原理，n个节点的图中，路径必然存在重复出现的顶点，也就是形成了环路。而SPFA仅在路径总权值变小时才会触发松弛更新，因此这个环路的总边权之和必然为负数，即存在负环。
二、基于最短路边数的判定证明
- 判定规则：维护cnt数组记录从起点到当前节点的最短路径经过的边数，若某点的cnt值≥n，则图中存在负环。
- 证明逻辑：
若某点的最短路径包含≥n条边，路径上的节点数至少为n+1，再次通过抽屉原理可推导出路径中必然存在重复顶点，也就是形成了环路。结合SPFA的松弛更新规则，只有路径总权值减小才会更新距离，因此该环路的边权和为负，直接判定存在负环。这种方式比统计入队次数效率更高，是工程中更常用的实现方案。
补充说明
为了能检测到图中任意位置的负环，算法初始化时会将所有节点直接加入队列，等价于在原图中新增一个虚拟源点，向所有节点连一条权值为0的边，保证原图中所有负环都能被虚拟源点可达，不会出现漏判的情况。
