标签：连通 int 命题 分量 问题 SAT define

SAT 问题

• SAT: Satisfiability 满足

• 给出很多个包含多个命题的条件，给出命题的真假方案，使得所有条件成立

• 如：对于命题 \(x_1,x_2,x_3,x_4,x_5…\) 使得 \(x_1∨¬x_2∨x_5\) 成立

2-SAT问题

• 每个条件包含两个命题的SAT问题

• 如：对于 \(x_1,x_2,x_3\) 使得 \(x_1∨x_3,¬x_2∨x_3\) 成立

• 转化：建图

• 用 \(x_i\) 表示 \(x_i=True\)，用 \(¬x_i\) 表示 \(x_i=False\)

• 用图论里的每一个点表示每一个命题，每一条边表示每两个命题间的推导关系

  • 推导关系：\(a→b⇔¬a∨b a,b∈True,False\)

  • 即：\(a∨b⇔¬a→b⇔¬b→a\)

  • 那么我们可以把每一个条件表示为图论中的边了

• 解的情况

• 无解：\(x_i→⋯→x_i∧¬x_i→…x_i\)

  • 即 \(x_i\) 和 \(¬x_i\) 在同一个强连通分量里，说明 \(x_i\)不管取真或假都是相反的，这就有问题了

• 有解：枚举所有 \(x_i\)，缩点找强连通分量，当 \(x_i\) 所在的强连通分量的拓扑排序在 \(¬x\) 所在的强连通分量的拓扑排序之后时，取 \(x\) 为 \(true\)

例题P4782 【模板】2-SAT 问题

#include<bits/stdc++.h>

#define rint register int
#define int long long
#define endl '\n'

using namespace std;

const int N = 2e6 + 5;
const int M = N;

int h[N],e[M],ne[M],idx,dfn[N],low[N],sk[N],ins[N],id[N],top,ts,n,m,cnt;

int inline min(int a,int b){
	return a<b?a:b;
}

void add(int a,int b){
    e[idx]=b,ne[idx]=h[a],h[a]=idx++;
}

void inline tarjan(int u){
    sk[++top]=u;ins[u]=1;
    dfn[u]=low[u]=++ts;
    for(rint i=h[u];~i;i=ne[i]){
        if(!dfn[e[i]]) {
            tarjan(e[i]);
            low[u]=min(low[e[i]],low[u]);
        }
        else if(ins[e[i]]){
            low[u]=min(dfn[e[i]],low[u]);
        }
    }
    if(dfn[u]==low[u]){
        int j;
        cnt++;
        do{
            j=sk[top--];
            id[j]=cnt;
            ins[j]=0;
        }
		while(j!=u);
    }
    return ;
}

signed main(){
    scanf("%lld%lld",&n,&m);
    memset(h,-1,sizeof h);
    while(m--){
        int i,a,j,b;
        scanf("%lld%lld%lld%lld",&a,&i,&b,&j);
        a--;
		b--;
        add(2*a+!i,2*b+j);
        add(2*b+!j,2*a+i);
    }
    
    for(rint i=0;i<2*n;i++){
        if(!dfn[i]){
        	tarjan(i);
		}
    }
    
    for(rint i=0;i<n;i++){
        if(id[i*2]==id[i*2+1]){
            puts("IMPOSSIBLE");
            return 0;
        }
    }
	
	puts("POSSIBLE");
	
    for(rint i=0;i<n;i++){
        if(id[i*2]<id[i*2+1]){
            printf("0 ");
        }
        else{
        	printf("1 ");
		}
    }
    
    return 0;
}

标签：连通,int,命题,分量,问题,SAT,define
来源： https://www.cnblogs.com/spaceswalker/p/16510471.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。