2-SAT 问题

2-SAT 问题是k-SAT问题在k==2时的特殊情况，因为已经证明k>=3时的k-sat问题属于npc问题。所以在这里仅研究2-SAT的特殊情况。

何为2-sat问题？

简单地说就是有N个集合，每个集合中有两个元素，其中一些集合中的元素存在相对关系。求出从每个集合中取出1个元素的方案。

先看一道例题：

COGS313

2-sat的最简单情况，选出一些元素时，一些元素不可选。做这些题时，一般会考虑建图或者用并查集之类的数据结构维护。但显然复杂度是无法接受的，考虑新的算法。

首先，如果A1，A2，B1，B2分别为两个集合的两个元素。

且存在以下的排斥关系。

A1<->B2

B1<->A2

那么考虑从A1向B1连边，这条边意味着选了A1就必须选B1，因为显然选B2是不合法的。考虑相反情况。如果选了B2，就必须选A2，因为B2不可以和A1共存。 B1<->A2也是这样处理。

这时候我们就得到了一个图。把图中的一个强连通分量取出考虑，这个强连通分量里的每个元素都可以代表这一整个强连通分量，即选了这个强连通分量中的一个元素就必须选这个强连通分量里的所有元素，强连通分量里的元素部分取出构成的方案是不合法的（自己思考为什么）。同时，如果一个集合中的两个元素都位于一个强连通分量中也是不合法的。这时候各个元素中的相对关系就很显然了，采用topsort做最后的处理。

//COGS 313
//by Cydiater
//2016.8.2
#include <iostream>
#include <cstdio>
#include <cstring>
#include <string>
#include <queue>
#include <map>
#include <algorithm>
#include <cstdlib>
#include <cmath>
#include <ctime>
#include <iomanip>
using namespace std;
#define ll long long
#define up(i,j,n)       for(int i=j;i<=n;i++)
#define down(i,j,n)     for(int i=j;i>=n;i--)
#define FILE "spo"
const int MAXN=1e5+5;
const int oo=0x3f3f3f3f;
inline int read(){
      char ch=getchar();int x=0,f=1;
      while(ch>‘9‘||ch<‘0‘){if(ch==‘-‘)f=-1;ch=getchar();}
      while(ch>=‘0‘&&ch<=‘9‘){x=x*10+ch-‘0‘;ch=getchar();}
      return x*f;
}
int N,M,LINK[MAXN],len=0,group[MAXN],dfn[MAXN],low[MAXN],dfs_clock=0,stack[MAXN],top=0,group_num=0,du[MAXN],opp[MAXN],LEN=0,Link[MAXN],q[MAXN],head,tail,lable[MAXN];
bool vis[MAXN];
struct edge{int x,y,next;}e[MAXN<<1],E[MAXN<<1];
namespace solution{
      inline void insert(int x,int y){e[++len].next=LINK[x];LINK[x]=len;e[len].y=y;e[len].x=x;}
      inline void Insert(int x,int y){E[++LEN].next=Link[x];Link[x]=LEN;E[LEN].y=y;E[LEN].x=x;}
      void init(){
            N=read();M=read();N<<=1;
            up(i,1,M){
                  int x=read()-1,y=read()-1;
                  insert(x,y^1);
                  insert(y,x^1);
            }
      }
      void tarjan(int node){
            dfn[node]=low[node]=++dfs_clock;
            stack[++top]=node;vis[node]=1;
            for(int i=LINK[node];i;i=e[i].next)
                  if(!dfn[e[i].y]){
                        tarjan(e[i].y);
                        low[node]=min(low[node],low[e[i].y]);
                  }
                  else if(vis[e[i].y])low[node]=min(low[node],dfn[e[i].y]);
            if(low[node]==dfn[node]){
                  int tmp;
                  group_num++;
                  do{
                        tmp=stack[top--];
                        vis[tmp]=0;
                        group[tmp]=group_num;
                  }while(tmp!=node);
            }
      }
      void slove(){
            memset(dfn,0,sizeof(dfn));
            memset(low,0,sizeof(low));
            memset(group,-1,sizeof(group));
            memset(du,0,sizeof(du));
            memset(lable,0,sizeof(lable));
            up(i,0,N-1)if(!dfn[i])tarjan(i);
            up(i,0,N-1){
                  if(group[i]==group[i^1]){
                        puts("NIE");
                        exit(0);
                  }
                  opp[group[i]]=group[i^1];
                  opp[group[i^1]]=group[i];
            }
            up(i,1,len){
                  int x=e[i].x,y=e[i].y;
                  if(group[x]!=group[y]){
                        Insert(group[y],group[x]);
                        du[group[x]]++;
                  }
            }
            head=1;tail=0;
            up(i,1,group_num)if(du[i]==0)q[++tail]=i;
            for(;head<=tail;head++){
                  int node=q[head];
                  if(lable[node]!=0)continue;
                  lable[node]=1;lable[opp[node]]=2;
                  for(int i=Link[node];i;i=E[i].next)
                        if(--du[E[i].y]==0)
                              q[++tail]=E[i].y;
            }
      }
      void output(){
            up(i,0,N-1)if(lable[group[i]]==1)printf("%d\n",i+1);
      }
}
int main(){
      //freopen("input.in","r",stdin);
      freopen(FILE".in","r",stdin);
      freopen(FILE".out","w",stdout);
      using namespace solution;
      init();
      slove();
      output();
      return 0;
}

POJ3207

这也是一道很简单的2-SAT题目，相比网络流2-SAT的题目更好看出模型..

这个相比上一题也更加简单，仅判断是否存在方案即可。

如果两个线段是相交的，那么两个线段同时在圆内或者圆外都是相交的。

这样就得到了约束关系，套用2-SAT的模板就行了。

//POJ 3207
//by Cydiater
//2016.8.2
#include <iostream>
#include <cstdio>
#include <cstdlib>
#include <cstring>
#include <string>
#include <algorithm>
#include <queue>
#include <map>
#include <algorithm>
#include <iomanip>
#include <string>
using namespace std;
#define ll long long
#define up(i,j,n)       for(int i=j;i<=n;i++)
#define down(i,j,n)     for(int i=j;i>=n;i--)
const int MAXN=1005;
const int oo=0x3f3f3f3f;
inline int read(){
      char ch=getchar();int x=0,f=1;
      while(ch>‘9‘||ch<‘0‘){if(ch==‘-‘)f=-1;ch=getchar();}
      while(ch>=‘0‘&&ch<=‘9‘){x=x*10+ch-‘0‘;ch=getchar();}
      return x*f;
}
int N,M,LINK[MAXN],len=0,st[MAXN],nd[MAXN],dfn[MAXN],low[MAXN],stack[MAXN],dfs_clock=0,top=0,group[MAXN],group_num=0;
bool vis[MAXN];
struct edge{int x,y,next;}e[MAXN<<10];
namespace solution{
      inline void insert(int x,int y){e[++len].next=LINK[x];LINK[x]=len;e[len].y=y;e[len].x=x;}
      void init(){
            N=read();M=read();
            up(i,0,M-1){
                  int x=read(),y=read();
                  st[i]=min(x,y);nd[i]=max(x,y);
            }
      }
      void build(){
            up(i,0,M-1)up(j,i+1,M-1){
                  if((st[i]>st[j]&&st[i]<nd[j]&&nd[i]>nd[j])||(st[j]>st[i]&&st[j]<nd[i]&&nd[j]>nd[i])){
                        insert(i,j+M);
                        insert(j+M,i);
                        insert(j,i+M);
                        insert(i+M,j);
                  }
            }
      }
      void tarjan(int node){
            low[node]=dfn[node]=++dfs_clock;
            vis[node]=1;stack[++top]=node;
            for(int i=LINK[node];i;i=e[i].next)
                  if(!dfn[e[i].y]){
                        tarjan(e[i].y);
                        low[node]=min(low[node],low[e[i].y]);
                  }
                  else if(vis[e[i].y]) low[node]=min(low[node],dfn[e[i].y]);
            if(low[node]==dfn[node]){
                  int tmp;group_num++;
                  do{
                        tmp=stack[top--];
                        vis[tmp]=0;
                        group[tmp]=group_num;
                  }while(tmp!=node);
            }
      }
      bool check(){
            up(i,1,M)if(group[i]==group[i+M])return 0;
            return 1;
      }
      void slove(){
            build();
            memset(dfn,0,sizeof(dfn));
            memset(low,0,sizeof(low));
            memset(vis,0,sizeof(vis));
            up(i,1,M<<1)if(!dfn[i])tarjan(i);
            if(check())puts("panda is telling the truth...");
            else       puts("the evil panda is lying again");
      }
}
int main(){
      //freopen("input.in","r",stdin);
      using namespace solution;
      init();
      slove();
      return 0;
}

POJ 3683

这道题调了两个多小时....

要注意几点，一是标记的下放，二是邻接表存储时不要打混...邻接表的命名打混这个真心是挺难查的...

题目本身不算难，2-SAT的裸题，拆点建图即可。

还有就是如果对于当前的约束条件，只要这个约束条件是存在的，不管哪个以为着必须的边是否正确，都要连边。

同时要注意到标记的下放。dfs即可。

//POJ 3683
//by Cydiater
//2016.8.2
#include <iostream>
#include <cstdio>
#include <cstdlib>
#include <queue>
#include <map>
#include <algorithm>
#include <ctime>
#include <map>
#include <iomanip>
#include <cstring>
#include <string>
using namespace std;
#define ll long long
#define up(i,j,n)       for(int i=j;i<=n;i++)
#define down(i,j,n)     for(int i=j;i>=n;i--)
const int MAXN=2005;
const int oo=0x3f3f3f3f;
inline int read(){
      char ch=getchar();int x=0,f=1;
      while(ch>‘9‘||ch<‘0‘){if(ch==‘-‘)f=-1;ch=getchar();}
      while(ch>=‘0‘&&ch<=‘9‘){x=x*10+ch-‘0‘;ch=getchar();}
      return x*f;
}
int N,st[MAXN],nd[MAXN],c[MAXN],LINK[MAXN],len=0,dfn[MAXN],low[MAXN],dfs_clock=0,stack[MAXN],top=0,group[MAXN],group_num=0,opp[MAXN],Link[MAXN],LEN=0,du[MAXN],q[MAXN<<5],head=1,tail=0;
int lable[MAXN];
bool vis[MAXN];
struct edge{int x,y,next;}e[MAXN*MAXN],E[MAXN*MAXN];
namespace solution{
      inline bool check(int st1,int nd1,int st2,int nd2){return (nd1<=st2)||(nd2<=st1);}
      inline void insert(int x,int y){e[++len].next=LINK[x];LINK[x]=len;e[len].y=y;e[len].x=x;}
      inline void Insert(int x,int y){E[++LEN].next=Link[x];Link[x]=LEN;E[LEN].y=y;E[LEN].x=x;}
      inline void print(int a,int b){
            if(a<10)printf("0%d:",a);
            else     printf("%d:",a);
            if(b<10)printf("0%d",b);
            else     printf("%d",b);
            printf(" ");
      }
      void init(){
            N=read();
            up(i,1,N){
                  int h1,m1,t1,h2,m2,t2,d;
                  scanf("%d:%d",&h1,&m1);
                  t1=h1*60+m1;
                  scanf("%d:%d",&h2,&m2);
                  t2=h2*60+m2;
                  st[i]=t1;nd[i]=t2;c[i]=read();
            }
      }
      void build(){
            up(i,1,N)up(j,i+1,N){
                  if(!check(st[i],st[i]+c[i],st[j],st[j]+c[j])){
                        insert(i,j+N);
                        insert(j,i+N);
                  }
                  if(!check(st[i],st[i]+c[i],nd[j]-c[j],nd[j])){
                        insert(i,j);
                        insert(j+N,i+N);
                  }
                  if(!check(nd[i]-c[i],nd[i],st[j],st[j]+c[j])){
                        insert(i+N,j+N);
                        insert(j,i);
                  }
                  if(!check(nd[i]-c[i],nd[i],nd[j]-c[j],nd[j])){
                        insert(i+N,j);
                        insert(j+N,i);
                  }
            }
      }
      void tarjan(int node){
            dfn[node]=low[node]=++dfs_clock;
            vis[node]=1;stack[++top]=node;
            for(int i=LINK[node];i;i=e[i].next)
                  if(!dfn[e[i].y]){
                        tarjan(e[i].y);
                        low[node]=min(low[node],low[e[i].y]);
                  }
                  else if(vis[e[i].y]) low[node]=min(low[node],dfn[e[i].y]);
            if(low[node]==dfn[node]){
                  int tmp;group_num++;
                  do{
                        tmp=stack[top--];
                        vis[tmp]=0;
                        group[tmp]=group_num;
                  }while(tmp!=node);
            }
      }
      void re_build(){
            up(i,1,N){
                  if(group[i]==group[i+N]){
                        puts("NO");
                        exit(0);
                  }
                  opp[group[i]]=group[i+N];
                  opp[group[i+N]]=group[i];
            }
            puts("YES");
            up(i,1,len){
                  int x=e[i].x,y=e[i].y;
                  if(group[x]==group[y])continue;
                  Insert(group[y],group[x]);
                  du[group[x]]++;
            }
      }
      void downit(int node){
            if(lable[node])return;
            lable[node]=-1;
            for(int i=Link[node];i;i=E[i].next)
                  downit(E[i].y);
      }
      void top_sort(){
            head=1;tail=0;
            up(i,1,group_num)if(du[i]==0)q[++tail]=i;
            for(;head<=tail;head++){
                  int node=q[head];
                  if(lable[node])continue;
                  lable[node]=1;downit(opp[node]);
                  for(int i=Link[node];i;i=E[i].next)
                        if(--du[E[i].y]==0)
                              q[++tail]=E[i].y;
            }
      }
      void slove(){
            memset(vis,0,sizeof(vis));
            memset(dfn,0,sizeof(dfn));
            memset(low,0,sizeof(low));
            memset(du,0,sizeof(du));
            memset(lable,0,sizeof(lable));
            build();
            up(i,1,N<<1)if(!dfn[i])tarjan(i);
            re_build();
            top_sort();
      }
      void output(){
            up(i,1,N){
                  if(lable[group[i]]==1){print(st[i]/60,st[i]%60);printf(" ");print((st[i]+c[i])/60,(st[i]+c[i])%60);}
                  else                  {print((nd[i]-c[i])/60,(nd[i]-c[i])%60);printf(" ");print(nd[i]/60,nd[i]%60);}
                  printf("\n");
            }
      }
}
int main(){
      freopen("input.in","r",stdin);
      using namespace solution;
      init();
      slove();
      output();
      return 0;
}

POJ 3678

题目大意是给N个点M条边，每个点可以是0或者1，每条边是一个操作，每个一边的操作对应一个值，问是否有可行的方案

2-SAT的模型通常都很好观察出来。

这里的建模需要注意两个点。

1.op==and而且res==1。

这时候A点必须是1，B点也必须是1，如何保证这一点？

if(op==1&&res==1){
　　insert(x,x+N);
　　insert(y,y+N);
}

2.op==XOR是不需要连边的。

我没搞懂为什么..但是好像是最后tarjan会自动的把那个xor的情况给处理掉。

//POJ 3678
//by Cydiater
//2016.8.3
#include <iostream>
#include <cstdio>
#include <cstdlib>
#include <cmath>
#include <ctime>
#include <queue>
#include <map>
#include <algorithm>
#include <cstring>
#include <string>
#include <algorithm>
using namespace std;
#define ll long long
#define up(i,j,n)       for(int i=j;i<=n;i++)
#define down(i,j,n)     for(int i=j;i>=n;i--)
const int MAXN=5005;
const int oo=0x3f3f3f3f;
inline int read(){
      char ch=getchar();int x=0,f=1;
      while(ch>‘9‘||ch<‘0‘){if(ch==‘-‘)f=-1;ch=getchar();}
      while(ch>=‘0‘&&ch<=‘9‘){x=x*10+ch-‘0‘;ch=getchar();}
      return x*f;
}
int N,M,LINK[MAXN],len=0,dfn[MAXN],low[MAXN],stack[MAXN],top=0,dfs_clock=0,group_num=0,group[MAXN];
bool vis[MAXN];
string s;
map<string,int>m;
struct edge{
      int x,y,next;
}e[MAXN<<10];
namespace solution{
      inline void insert(int x,int y){e[++len].next=LINK[x];LINK[x]=len;e[len].y=y;}
      void init(){
            m["AND"]=1;m["OR"]=2;m["XOR"]=3;
            N=read();M=read();
            up(i,1,M){
                  int x=read(),y=read(),res=read();cin>>s;
                  int op=m[s];
                  if(op==1&&res==1){
                        insert(x,x+N);
                        insert(y,y+N);
                  }
                  if(op==1&&res==0){
                        insert(x+N,y);
                        insert(y+N,x);
                  }
                  if(op==2&&res==1){
                        insert(x,y+N);
                        insert(y,x+N);
                  }
                  if(op==2&&res==0){
                        insert(x+N,x);
                        insert(y+N,y);
                  }
                  if(op==3&&res==1){
                        insert(x,y+N);
                        insert(y,x+N);
                        insert(y+N,x);
                        insert(x+N,y);
                  }
                  if(op==3&&res==0){
                        insert(x,y);
                        insert(y,x);
                        insert(x+N,y+N);
                        insert(y+N,x+N);
                  }
            }
      }
      void tarjan(int node){
            dfn[node]=low[node]=++dfs_clock;
            stack[++top]=node;vis[node]=1;
            for(int i=LINK[node];i;i=e[i].next)
                  if(!dfn[e[i].y]){
                        tarjan(e[i].y);
                        low[node]=min(low[node],low[e[i].y]);
                  }else if(vis[e[i].y]) low[node]=min(low[node],dfn[e[i].y]);
            if(low[node]==dfn[node]){
                  group_num++;
                  int tmp;
                  do{
                        tmp=stack[top--];
                        vis[tmp]=0;
                        group[tmp]=group_num;
                  }while(tmp!=node);
            }
      }
      bool check(){
            up(i,0,N-1)if(group[i]==group[i+N])return 0;
            return 1;
      }
      void slove(){
            memset(dfn,0,sizeof(dfn));
            memset(low,0,sizeof(low));
            memset(vis,0,sizeof(vis));
            up(i,1,N<<1)if(!dfn[i])tarjan(i);
            if(check())puts("YES");
            else       puts("NO");
      }
}
int main(){
      //freopen("input.in","r",stdin);
      using namespace solution;
      init();
      slove();
      return 0;
}

最后一道2-SAT题目！

POJ2749

首先一些hate和friend的约束条件建图，然后根据二分出来的最长距离，对于i,j之间所有可能的路径:

i-S1-j

i-S2-j

i-S1-S2-j

i-S2-S1-j

如果存在大于lim的，也加入到约束条件中，判一下就行了。

//POJ 2749
//by Cydiater
//2016.8.8
#include <iostream>
#include <cstdio>
#include <cstring>
#include <string>
#include <algorithm>
#include <queue>
#include <map>
#include <iomanip>
#include <ctime>
#include <cmath>
#include <cstdlib>
using namespace std;
#define ll long long
#define up(i,j,n)       for(int i=j;i<=n;i++)
#define down(i,j,n)     for(int i=j;i>=n;i--)
typedef pair<int,int> pii;
const int MAXN=2005;
const int oo=0x3f3f3f3f;
inline int read(){
      char ch=getchar();int x=0,f=1;
      while(ch>‘9‘||ch<‘0‘){if(ch==‘-‘)f=-1;ch=getchar();}
      while(ch>=‘0‘&&ch<=‘9‘){x=x*10+ch-‘0‘;ch=getchar();}
      return x*f;
}
pii S1,S2,node[MAXN],hate[MAXN],fri[MAXN];
int N,A,B,leftt,rightt,mid,LINK[MAXN],len,dfn[MAXN],low[MAXN],stack[MAXN],top,dfs_clock,group[MAXN],group_num;
bool vis[MAXN];
struct edge{int x,y,next;}e[MAXN<<10];
namespace solution{
      inline int dist(pii a,pii b){return abs(a.first-b.first)+abs(a.second-b.second);}
      inline void insert(int x,int y){e[++len].next=LINK[x];LINK[x]=len;e[len].y=y;e[len].x=x;}
      void init(){
            N=read();A=read();B=read();
            int x=read(),y=read();
            S1=make_pair(x,y);
            x=read();y=read();
            S2=make_pair(x,y);
            up(i,1,N){
                  int x=read(),y=read();
                  node[i]=make_pair(x,y);
            }
            up(i,1,A){
                  int x=read(),y=read();
                  hate[i]=make_pair(x,y);
            }
            up(i,1,B){
                  int x=read(),y=read();
                  fri[i]=make_pair(x,y);
            }
      }
      void tarjan(int node){
            stack[++top]=node;vis[node]=1;
            low[node]=dfn[node]=++dfs_clock;
            for(int i=LINK[node];i;i=e[i].next)
                  if(!dfn[e[i].y]){
                        tarjan(e[i].y);
                        low[node]=min(low[node],low[e[i].y]);
                  }else if(vis[e[i].y])   low[node]=min(low[node],dfn[e[i].y]);
            if(dfn[node]==low[node]){
                  group_num++;int tmp;
                  do{
                        tmp=stack[top--];
                        vis[tmp]=0;
                        group[tmp]=group_num;
                  }while(tmp!=node);
            }
      }
      bool check(int lim){
            len=0;top=0;dfs_clock=0;group_num=0;
            memset(LINK,0,sizeof(LINK));
            memset(dfn,0,sizeof(dfn));
            memset(low,0,sizeof(low));
            memset(vis,0,sizeof(vis));
            up(i,1,A){
                  int x=hate[i].first,y=hate[i].second;
                  insert(x,y+N);
                  insert(y,x+N);
                  insert(x+N,y);
                  insert(y+N,x);
            }
            up(i,1,B){
                  int x=fri[i].first,y=fri[i].second;
                  insert(x,y);
                  insert(y,x);
                  insert(x+N,y+N);
                  insert(y+N,x+N);
            }
            up(i,1,N)up(j,i+1,N){
                  if(dist(node[i],S1)+dist(S1,node[j])>lim){
                        insert(i,j+N);
                        insert(j,i+N);
                  }
                  if(dist(node[i],S2)+dist(S2,node[j])>lim){
                        insert(i+N,j);
                        insert(j+N,i);
                  }
                  if(dist(node[i],S1)+dist(S1,S2)+dist(S2,node[j])>lim){
                        insert(i,j);
                        insert(j+N,i+N);
                  }
                  if(dist(node[i],S2)+dist(S1,S2)+dist(S1,node[j])>lim){
                        insert(i+N,j+N);
                        insert(j,i);
                  }
            }
            up(i,1,N<<1)if(!dfn[i])tarjan(i);
            up(i,1,N)if(group[i]==group[i+N])return 0;
            return 1;
      }
      void slove(){
            leftt=0;rightt=10000000;
            while(leftt+1<rightt){
                  mid=(leftt+rightt)>>1;
                  if(check(mid))    rightt=mid;
                  else              leftt=mid;
            }
            if((!check(leftt))&&(!check(rightt)))puts("-1");
            else if(check(leftt))  printf("%d\n",leftt);
            else              printf("%d\n",rightt);
      }
}
int main(){
      //freopen("input.in","r",stdin);
      using namespace solution;
      init();
      slove();
      return 0;
}
时间： 2024-11-07 09:57:44

2-SAT 问题的相关文章

LA 3211 飞机调度（2—SAT）

https://vjudge.net/problem/UVALive-3211 题意: 有n架飞机需要着陆,每架飞机都可以选择“早着陆”和“晚着陆”两种方式之一,且必须选择一种,第i架飞机的早着陆时间为E,晚着陆时间为L,不得在其他时间着陆.你的任务是为这些飞机安排着陆方式,使得整个着陆计划尽量安全.换句话说,如果把所有飞机的实际着陆时间按照从早到晚的顺序排列,相邻两个着陆时间间隔的最小值. 思路: 二分查找最大值P,每次都用2—SAT判断是否可行. 1 #include<iostream>

8.3吝啬SAT问题

吝啬SAT问题是这样的:给定一组子句(每个子句都是其中文字的析取)和整数k,求一个最多有k个变量为true的满足赋值--如果该赋值存在.证明吝啬SAT是NP-完全问题. 1.易知吝啬SAT的解可以在多项式时间内验证,因此属于NP问题. 2.如果我们把吝啬SAT问题中的k设置为输入的数目,那么SAT问题就可以规约到吝啬SAT问题,所以吝啬SAT问题是np-完全问题.

POJ 3207 Ikki&#39;s Story IV - Panda&#39;s Trick（2 - sat啊）

题目链接:http://poj.org/problem?id=3207 Description liympanda, one of Ikki's friend, likes playing games with Ikki. Today after minesweeping with Ikki and winning so many times, he is tired of such easy games and wants to play another game with Ikki. liy

多边形碰撞 -- SAT方法

检测凸多边形碰撞的一种简单的方法是SAT(Separating Axis Theorem),即分离轴定理. 原理:将多边形投影到一条向量上,看这两个多边形的投影是否重叠.如果不重叠,则认为这两个多边形是分离的,否则找下一条向量来继续投影.我们不需要比较很多条向量,因为已经在数学上证明,多边形每条边的垂直向量就是我们需要的向量. 1.AABB 让我们首先以AABB开始(AABB是一种两边分别平行于X-Y轴的矩形) 判断两个AABB是否碰撞,我们只需要投影两次,分别是投影在平行于X轴和Y轴的向量上

hdu 4751 Divide Groups 2—sat问题 还是未理解

Divide Groups Time Limit: 2000/1000 MS (Java/Others)    Memory Limit: 32768/32768 K (Java/Others) Total Submission(s): 1443    Accepted Submission(s): 512 Problem Description This year is the 60th anniversary of NJUST, and to make the celebration mor

HIT 1917 2—SAT

题目大意:一国有n个党派,每个党派在议会中都有2个代表, 现要组建和平委员会,要从每个党派在议会的代表中选出1人,一共n人组成和平委员会. 已知有一些代表之间存在仇恨,也就是说他们不能同时被选为和平委员会的成员, 现要你判断满足要求的和平委员会能否创立?如果能,请任意给出一种方案.( POI 0106 ) ----------------------------------------- 这道题就是裸的2-SAT 不过我用了tarjan缩点 然后一波拓排 tips:一个问题无解当且仅当一个集合的

2—SAT问题

现有一个由N个布尔值组成的序列A,给出一些限制关系,比如A[x] AND A[y]=0.A[x] OR A[y] OR A[z]=1.A[x] XOR A[y]=0等,要确定A[0..N-1]的值,使得其满足所有限制关系.这个称为SAT问题,特别的,若每种限制关系中最多只对两个元素进行限制,则称为2-SAT问题. 对于x.y有11种关系,将其拆点2x(假),2x+1(真).对于x为假或者y为假这样的条件,我们连两条有向边2x+1->2y.2y+1->2x,注意这里是有向边以及边的起点和终点的关

SAT考试里最难的数学题？ &middot; 三只猫的温暖

问题 今天无意中在Quora上看到有人贴出来一道号称是SAT里最难的一道数学题,一下子勾起了我的兴趣.于是拿起笔来写写画画,花了差不多十五分钟搞定.觉得有点意思,决定把解题过程记下来.原帖的图太小,我用GeoGebra重新画了一遍.没错,我就是强迫症. 为了省事,就把这道题叫做RASBTC. In the figure above, arc (text{SBT}) is one quarter of a circle with center (text{R}) and radius 6. If

SAT求解器变元活跃度计算模式的切换

变元活跃度计算模式有:VSIDS.基于历史出现时刻与当前冲突时刻距离等 有三个最小堆: // A priority queue of variables ordered with respect to the variable activity. Heap<VarOrderLt> order_heap_CHB,                                order_heap_VSIDS, order_heap_distance; 一般的求解切换方式是: conflicts

SAT求解器快速入门

从事组合优化或信息安全方向的研究人员,基于SMT研究,需要快速学习SAT求解器的基本原理和方法.以下是快速入门的几点体会: 1.理清需要——是完备求解器还是不完备求解器 完备求解器 能给出SAT.UNSAT.unknow三种确定的答案,尤其是UNSAT结论能给出证明推导过程,指出导致矛盾的关键路径.   不完备求解器能给出SAT.unknow两种结论.SAT结论给出一组可满足解即完成求解任务.可能会存在其他一组或多组可满足解.如果问题本身不知一组解,那么不同的求解器得出的可满足解可能不同. 2.