将 3-SAT 在多项式时间内归约到彩虹路径喵！

人：【彩虹路径】这个怎么做/kel

我：……这个是不是不太可做，我试试把 3-SAT 规约过来……

我：做完了，这个是 NP-hard。

问题：给定一个无向图，每个边有颜色（？？色图？？）。给定起点和终点，求是否存在一条起点到终点的路径满足边的颜色两两不同。

注：下面为了表述方便，描述边的时候使用了箭头。实际的图是无向的。

我们考虑把 3-SAT 规约到这个问题。

首先我们造出选择器：可以从若干个中选择一条走。就是类似 s\to x_1\to x_2\to x_3\to \dots\to t,s\to y_1\to y_2\to y_3\to \dots\to t,\dots 的形式。可以从 x,y,\dots 中选择一个。

3-SAT 有未知数！我们用选择器来造未知数。s_0\to x_1\to s_1,s_0\to \overline{x_1}\to s_1 代表 x_1 是否选择，同理有 x_2,x_3,\dots。需要保证颜色两两不同。我们不会用到 x\to s 的边，只用 s\to x。

如果允许重边，那么其实 x 可以直接删掉而变成边。

3-SAT 有条件！对于合取显然是若干个东西首尾相接。那么我们考虑一个析取怎么做。

比如说假设是 x_1\lor \overline{x_2}\lor x_3，那么 s\to \overline{x_1}\to t,s\to x_2\to t,s\to \overline{x_3}\to t。就做完了！

注意这样有一个小问题就是可能多个析取式使用了相同颜色的边，此时可以在上面的变量选择器中把一条边替换为多条来解决。

最终点数和边数都是 O(n+m)，规约用时也是 O(n+m)（可能会多 \log），做完了。

小练习：对于 (x_1\lor \overline{x_2}\lor x_3)\land (x_1\lor x_2\lor \overline{x_4})\land (\overline{x_2}\lor x_3\lor x_4) 建图。

后续：

人：【若干假做法】