UTPC2013 E 2-SAT

問題

日本語なので本文参照（http://utpc2013.contest.atcoder.jp/tasks/utpc2013_05）

変数がn, 節の数がm以下の乗法標準形の論理式が与えられる。
（よくある2-SATの(x1 or x2) and (~x3 or x4) and ...みたいな形という意味）

この式に対して変数の割り当てが与えられる。
変数の割り当てを10個以下変更して、式をtrueにできるなら、
変更するべき変数の個数の最小値を、できないならできないと出力せよ。

制約条件

n≦10000
m≦100000

方針

式がfalseであるということは、節のどこかがfalseなので、
最初にfalseになっている節で変数二通りどちらかの割り当てを変更するということを
10回以内やって、式がtrueになるかをみてやればいい。

全探索で間に合うっぽい。

ソースコード

const int MX = 100000;
int n, m, L[MX], R[MX];
char expr[MX * 20], assign[10010];
 
bool cur_assign[MX];
 
int in(int &pos){
	if(expr[pos] == '~'){
		pos++;
		return -in(pos);
	}
	int d = 0;
	while(isdigit(expr[pos])){
		d *= 10;
		d += expr[pos++] - '0';
	}
	return d;
}
int main(){
	scanf("%d%d", &n, &m);
	scanf("%s", expr);
	scanf("%s", assign);
	
	int pos = 0;
	rep(i, m){
		pos++;
		L[i] = in(pos); pos++;
		R[i] = in(pos); pos += 2;
	}
	//rep(i, m) cerr<<L[i]<<" "<<R[i]<<endl;
	int ans = inf;
	
	rep(bit, 1 << 10){
		
		rep(i, n) cur_assign[i + 1] = assign[i] == 'T';
		
		rep(it, 11){
			
			rep(i, m){
				int lpos = abs(L[i]), rpos = abs(R[i]);
				int l = cur_assign[lpos] ^ (L[i] < 0);
				int r = cur_assign[rpos] ^ (R[i] < 0);
				
				if(l || r) continue;
				if(it == 10) goto FAIL;
				
				if(bit >> it & 1){
					if(l) goto FAIL;
					cur_assign[lpos] ^= 1;
				}
				else{
					if(r) goto FAIL;
					cur_assign[rpos] ^= 1;
				}
				goto NEXT;
			}
			ans = min(ans, it);
			break;
			
			NEXT:;
		}
		FAIL:;
	}
	if(ans > 10) cout << "TOO LARGE" << endl;
	else cout << ans << endl;
	
	return 0;
}