2-SAT問題まとめ
6600 ワード
2-SAT問題まとめ
2-SAT問題:n個のブール型の変数は、m個の制約条件を与え、制約条件は例えば:A,Bは同時に真ではなく、A,Bは同時に真でなければならない.
アルゴリズム入門経典における解決策を見たが,この解決策については比較的理解しやすく,効率もよい.n個の変数がn*2個の変数に分解された図G、すなわちxiがxi*2とxi*2+1で表され、前者が1であればxiが真であり、後者が1であればxiが偽であることを示す.制約条件については、例えばxiが偽であるかxjが偽であるか、すなわちxiが偽xjが真であるか、xjが偽xiが真であるかの2つの有向辺が得られ、xi*2+1->xj*2 xj*2+1->xi*2が得られ、有向図Gが得られる.
有向図中のすべての有向辺は肯定的にいくつかの連通成分を構成しており、ある連通成分のうち、一点が1であれば、この連通成分のすべての点が1であり、逆に、ある点が1であり、0であれば、mの制約条件が矛盾しているに違いないので、この問題は解決できない.
このプロセスをシミュレートするときにdfsを使用します.一点からこの点を0と仮定し、この点から到達可能なすべての点を巡り、マークします.マークしているうちに点が1であることが発見されたら、この点を1とし、この点を1として巡り始めます.この点が1を0とすると矛盾します.では、上記の問題が発生し、制約条件が矛盾し、問題が解決できない.
転載先:https://www.cnblogs.com/wuwangchuxin0924/p/6433177.html
2-SAT問題:n個のブール型の変数は、m個の制約条件を与え、制約条件は例えば:A,Bは同時に真ではなく、A,Bは同時に真でなければならない.
アルゴリズム入門経典における解決策を見たが,この解決策については比較的理解しやすく,効率もよい.n個の変数がn*2個の変数に分解された図G、すなわちxiがxi*2とxi*2+1で表され、前者が1であればxiが真であり、後者が1であればxiが偽であることを示す.制約条件については、例えばxiが偽であるかxjが偽であるか、すなわちxiが偽xjが真であるか、xjが偽xiが真であるかの2つの有向辺が得られ、xi*2+1->xj*2 xj*2+1->xi*2が得られ、有向図Gが得られる.
有向図中のすべての有向辺は肯定的にいくつかの連通成分を構成しており、ある連通成分のうち、一点が1であれば、この連通成分のすべての点が1であり、逆に、ある点が1であり、0であれば、mの制約条件が矛盾しているに違いないので、この問題は解決できない.
このプロセスをシミュレートするときにdfsを使用します.一点からこの点を0と仮定し、この点から到達可能なすべての点を巡り、マークします.マークしているうちに点が1であることが発見されたら、この点を1とし、この点を1として巡り始めます.この点が1を0とすると矛盾します.では、上記の問題が発生し、制約条件が矛盾し、問題が解決できない.
/*********************************************2-SAT *********************************************/
const int maxn=10000+10;
struct TwoSAT
{
int n;// ( )
vector<int> G[maxn*2];//G[i].j mark[i]=true, mark[j] =true
bool mark[maxn*2];//
int S[maxn*2],c;//S c dfs
// x dfs ,
// , false
bool dfs(int x)
{
if(mark[x^1]) return false;//
if(mark[x]) return true;
mark[x]=true;
S[c++]=x;
for(int i=0;i)
if(!dfs(G[x][i])) return false;
return true;
}
void init(int n)
{
this->n=n;
for(int i=0;i<2*n;i++)
G[i].clear();
memset(mark,0,sizeof(mark));
}
// (x,xval) (y,yval)
//xval=0 ,yval=1
void add_clause(int x,int xval,int y,int yval)// ,
{
x=x*2+xval;
y=y*2+yval;
G[x^1].push_back(y);
G[y^1].push_back(x);
}
// 2-SAT
bool solve()
{
for(int i=0;i<2*n;i+=2)
if(!mark[i] && !mark[i+1])
{
c=0;
if(!dfs(i))
{
while(c>0) mark[S[--c]]=false;
if(!dfs(i+1)) return false;
}
}
return true;
}
};
/*********************************************2-SAT *********************************************/
転載先:https://www.cnblogs.com/wuwangchuxin0924/p/6433177.html