题目大意：给出一个无向图，保证这个图有哈密顿回路，求这个图是不是平面图。

思路：平面图的判定条件之一：如果边数大于点数*3+6那么这个图一定不是平面图。这算是一个强剪枝吧。

我们把图中哈密顿回路的这个环上的边去掉，就变成了判定边能否不想交的2-SAT问题，POJ好像有一个原题来着。建图方法我就不说了，相信大家看到2-SAT就知道怎么写了。

CODE：

#include <cstdio>
#include <cstring>
#include <iostream>
#include <algorithm>
#define MAX 10010
using namespace std;
 
struct Edge{
    int x,y;
     
    Edge(int _,int __):x(_),y(__) {}
    Edge() {}
    void Read() {
        scanf("%d%d",&x,&y);
    }
}edge[MAX],stack[MAX];
int top;
 
int cases,points,edges;
int C[MAX];
 
inline bool Judge(const Edge &a,const Edge &b)
{
    return b.x > a.x && b.x < a.y && b.y > a.y;
}
 
namespace II_SAT{
    int head[MAX],total;
    int next[819200],aim[819200];
     
    int dfn[MAX],low[MAX],_clock;
    int stack[MAX],top;
    bool in_stack[MAX];
    int changed[MAX],scc;
     
    void Initialize() {
        total = _clock = scc = top = 0;
        memset(head,0,sizeof(head));
        memset(dfn,0,sizeof(dfn));
        memset(in_stack,false,sizeof(in_stack));
    }
    void Add(int x,int y) {
        next[++total] = head[x];
        aim[total] = y;
        head[x] = total;
    }
    void Tarjan(int x) {
        dfn[x] = low[x] = ++_clock;
        stack[++top] = x;
        in_stack[x] = true;
        for(int i = head[x]; i; i = next[i]) {
            if(!dfn[aim[i]])
                Tarjan(aim[i]),low[x] = min(low[x],low[aim[i]]);
            else if(in_stack[aim[i]])
                low[x] = min(low[x],dfn[aim[i]]);
        }
        if(dfn[x] == low[x]) {
            ++scc;
            int temp;
            do {
                temp = stack[top--];
                in_stack[temp] = false;
                changed[temp] = scc;
            }while(temp != x);
        }
    }
}
 
int main()
{
    for(cin >> cases; cases--;) {
        scanf("%d%d",&points,&edges);
        for(int i = 1; i <= edges; ++i)
            edge[i].Read();
        for(int x,i = 1; i <= points; ++i) {
            scanf("%d",&x);
            C[x] = i;
        }
        if(edges > 3 * points + 6) {
            puts("NO");
            continue;
        }
        top = 0;
        for(int i = 1; i <= edges; ++i) {
            int s = C[edge[i].x],t = C[edge[i].y];
            if(s > t)    swap(s,t);
            if(!((s + 1 == t) || (s == 1 && t == points)))
                stack[++top] = Edge(s,t);
        }
        II_SAT::Initialize();
        for(int i = 1; i <= top; ++i)
            for(int j = i + 1; j <= top; ++j)
                if(Judge(stack[i],stack[j]) || Judge(stack[j],stack[i])) {
                    II_SAT::Add(i << 1,j << 1|1);
                    II_SAT::Add(j << 1|1,i << 1);
                    II_SAT::Add(j << 1,i << 1|1);
                    II_SAT::Add(i << 1|1,j << 1);
                }
        for(int i = 2; i <= (top << 1|1); ++i)
            if(!II_SAT::dfn[i])
                II_SAT::Tarjan(i);
        bool flag = true;
        for(int i = 1; i <= top; ++i)
            if(II_SAT::changed[i << 1] == II_SAT::changed[i << 1|1]) {
                flag = false;
                break;
            }
        puts(&"NO\0YES"[flag * 3]);
    }
    return 0;
}

BZOJ 1997 HNOI 2010 Planar 2-SAT