问题简介

在计算机科学中，布尔可满足性问题（有时称为命题可满足性问题，缩写为SATISFIABILITY或SAT）是确定是否存在满足给定布尔公式的解释的问题。换句话说，它询问给定布尔公式的变量是否可以一致地用值TRUE或FALSE替换，公式计算结果为TRUE。如果是这种情况，公式称为可满足。另一方面，如果不存在这样的赋值，则对于所有可能的变量赋值，公式表示的函数为FALSE，并且公式不可满足。例如，公式“a AND NOT b”是可以满足的，因为可以找到值a = TRUE且b = FALSE，这使得（a AND NOT b）= TRUE。相反，“a AND NOT a”是不可满足的。——百度百科

在每个限制中牵扯到的最多的元素假设是，我们就称为问题。可以证明当时为完全问题。下面只讨论的情况。

引入

从一个最简单的问题开始今天的讨论

有n对夫妻被邀请参加一个聚会，因为场地的问题，每对夫妻中只有1人可以列席。在2n 个人中，某些人之间有着很大的矛盾（当然夫妻之间是没有矛盾的），有矛盾的2个人是不会同时出现在聚会上的。有没有可能会有n 个人同时列席？——hdu3062

对于每对夫妻，我们可以将丈夫去看作，妻子去看作。要求给每对夫妻确定一个值，使得满足这个限制。

这就是最简单的模型。

构图

先观察这些限制,假设A中的丈夫不能和B中的妻子一起去(？？？)。那么也就是说，A中的丈夫只能和B中的丈夫一起去。也就是说，如果A中的丈夫去，那么B中的丈夫也必须去。同理，如果B中的妻子去，那么A中的妻子也必须去。
我们就从A中的丈夫向B中的丈夫连一条边，从B中的妻子向A中的妻子连一条边，表示这些"必须"的条件。

显然我们就可以得到这样一个结论:如果一个点被选了，那么这个点所能到达的所有点也必须被选择。如果一个点没选，那么所有可以到达这个点的点都不能选。出现矛盾当且仅当某对夫妻的丈夫和妻子都必须去。

算法

暴力解法

我们枚举每一个人选或者不选，然后去查看是否会出现矛盾。
如果一对夫妻中两个人不论选择谁都会出现矛盾。那么问题必定无解。

优化

继续推一些结论。
对于同一个强连通分量里的点，如果选择其中一个，那么这个强连通分量中的点必须全部选择。这样我们可以先缩点。如果一对夫妻出现在了同一个强连通分量里面肯定无解。否则一定有解。
找可行解可以先拓扑排序一下，然后自底向上的顺序推导。

证明

观察我们的构图方式可以发现构出来的图有对称性。
啥是对称性？？

如图。我们观察其中的一组点，比如

发现可以到达的点是,可以到达的点是,而可以到达的点是,可以到达的点是。刚好对称。也就是说我们只要保证可以到达的不会矛盾，那么就可以保证可以到达的点不会矛盾。我们如果选择了，那么就一定选择，这时把和都删去。**按照这种思路，我们每次找到一个未确定的点，使得到达的点中没有(即x的对立点)。**
这样我们一定可以找到一组解。而无解的情况也就是找不到这种点的时候。即一对点存在于同一个强连通分量中。
然后思考求解的过程，因为要使得“到达的点中没有(即x的对立点)。”
所以可以拓扑排序。然后就自底向上的找答案。
有一种更加简单的找可行解的方法。

注意到算法的本质是一次，他在回溯时会优先取出有向图"底部"的进行标记。故算法得到的编号本身就已经满足缩点后的有向无环图中"自底向上"的拓扑序。——《算法竞赛进阶指南》

得出结论：直接比较缩点之后编号的大小就可以得出答案，较小的为1，较大的为0。

资料

我讲的不好？？
没关系，再看些资料吧。
https://blog.csdn.net/qq_24451605/article/details/47126143
由对称性解2-sat问题

代码

/*
* @Author: wxyww
* @Date:   2019-04-28 18:50:21
* @Last Modified time: 2019-04-28 19:59:02
*/
#include<cstdio>
#include<iostream>
#include<cstdlib>
#include<cstring>
#include<algorithm>
#include<queue>
#include<vector>
#include<ctime>
using namespace std;
typedef long long ll;
const int N = 2010;
ll read() {
    ll x=0,f=1;char c=getchar();
    while(c<'0'||c>'9') {
        if(c=='-') f=-1;
        c=getchar();
    }
    while(c>='0'&&c<='9') {
        x=x*10+c-'0';
        c=getchar();
    }
    return x*f;
}
struct node{
    int v,nxt;
}e[1000000];
int n,m,ejs,head[N];
void add(int u,int v) {
    e[++ejs].v = v;e[ejs].nxt = head[u];head[u] = ejs;
}
int vis[N],tot,dfn[N],low[N],sta[N],coljs,top,col[N];
void tarjan(int u) {
    dfn[u] = low[u] = ++tot;
    sta[++top] = u;vis[u] = 1;
    for(int i = head[u];i;i = e[i].nxt) {
        int v = e[i].v;
        if(!dfn[v]) {
            tarjan(v);
            low[u] = min(low[u],low[v]);
        }
        else if(vis[v]) low[u] = min(low[u],low[v]);
    }
    if(low[u] == dfn[u]) {
        ++coljs;
        do {
            int x = sta[top--];
            col[x] = coljs;
            vis[x] = 0;
        }while(sta[top + 1] != u);
    }
}
int main() {    
    while(~scanf("%d%d",&n,&m)) {
   memset(head,0,sizeof(head));
   ejs = 0;
   coljs = 0;
   memset(dfn,0,sizeof(dfn));memset(low,0,sizeof(low));
   tot = 0;top = 0;

    for(int i = 1;i <= m;++i) {
        int x = read() + 1,y = read() + 1;
        int c1 = read(),c2 = read();
        if(c1) {
            if(c2) add(x + n, y),add(y + n,x);
            else add(x + n,y + n),add(y,x);
        }
        else {
            if(c2) add(x, y),add(y + n,x + n);
            else add(x,y + n),add(y,x + n);
        }
    }

    for(int i = 1;i <= n + n;++i) if(!dfn[i]) tarjan(i);
    int bz = 0;
    for(int i = 1;i <= n;++i) {
        if(col[i] == col[i + n]) {
            bz = 1;break;
        }
    }
    puts(bz ? "NO" : "YES");
}
    return 0;
}