Codeforces #317 Div1 C. CNF 2

この回はまともにCを考える時間もなかった。
http://codeforces.com/contest/571/problem/C

問題

ブール代数におけるCNF(連言標準形)を考える。
N個のブール値変数V[i]に対し、CNFとは、複数の節のandで構成された式で、個々の節は変数または変数の否定のorの形で表現できるものである。

ここで式中に各変数は最大2回しか登場しないとする。
そのようなCNFが与えられるので、式の評価が真となる変数の真偽値の組み合わせが存在すればそれを答えよ。

解法

式中1度も出てこない変数は真でも偽でもよいり、式中1回しか出てこない、または2回出るが2回とも否定の有無が一致する場合、その節が真となる値を割り振ればよい。
問題は、変数が式中2回出てきて、片方は否定で片方は否定でない場合である。
以下そのような変数を未確定の変数と呼ぶ。

未確定の変数がa個ある場合、未確定の節は最大2a個である。
ここで、そのような未確定変数と未確定節からなる二部グラフを考える。
未確定の変数は真偽どちらかの値しか取れないので、1つの変数は1つの節を真にできる。
と考えると、変数と節のマッチングは節の数と一致しなければならない。

ここで節の数をbとする。前記の条件よりb≦aである。
もし節に1個しか辺がない場合、その節は辺の先にある変数とマッチさせなければならない。
そのような節がすべてマッチングでき、残された節はすべて2個以上マッチング対象の辺が残っているとする。
その場合、ホールの結婚定理より適当にマッチングしても節はすべてマッチングできる。

上記をまとめると、以下のようにしていけば良い。
まず各節について、priority queueを用いてそこにつながる未確定変数の少ない順に処理を進める。
もしつながる未確定変数が0個の節が現れた場合、式の評価が真にはできない。

そうでない場合、つながる未確定変数を1個選び、節が真となるようその変数の真偽を確定させる。
もしその変数が、別の節に否定の有無が逆の項を含む場合、その節からは未確定変数が1個減ることになる。
上記処理を節がなくなるまで繰り返せばよい。

int N,M;
set<int> V[303030];
int vv[303030];
int pos[603030];
int vis[303030];


void solve() {
	int i,j,k,l,r,x,y; string s;
	
	cin>>N>>M;
	priority_queue<pair<int,int> > q;
	
	for(i=1;i<=N;i++) {
		cin>>x;
		FOR(j,x) {
			cin>>y;
			V[i].insert(y);
			pos[300000+y]=i;
		}
		q.push({-V[i].size(),i});
	}
	
	while(q.size()) {
		auto r=q.top();
		int cur=r.second;
		q.pop();
		
		if(vis[cur]) continue;
		vis[cur]=1;
		
		if(V[cur].empty()) return _P("NO\n");
		
		x=*V[cur].begin();
		vv[abs(x)]=x>0;
		
		if(pos[300000-x]>0) {
			V[pos[300000-x]].erase(-x);
			q.push({-V[pos[300000-x]].size(),pos[300000-x]});
		}
	}
	
	_P("YES\n");
	for(i=1;i<=M;i++) _P("%d",vv[i]);
	_P("\n");
}

まとめ

考察パートはともかく、実装はわりとあっさり。