2-SAT 除了 Tarjan 缩点+拓扑排序 以外有一种解法：枚举所有值的状态，若搜索到一种可行状态就退出，即暴力染色。

这种解法可以搜到字典序最小的解。

我的疑问是：这种解法的时间复杂度如何证明是 $O(nm)$？感性理解不难证明时间复杂度约为 $O(nm)$，但是实际运行时间往往低很多。

网上搜不到类似的证明。求助。

顺便捞一下远古遗留问题，见此贴。