UTPC 2013 : E - 2-SAT

これは本番解けたかも。
http://utpc2013.contest.atcoder.jp/tasks/utpc2013_05

問題

文字列の形でM節からなる2SATの式が与えられる。
また、各変数の初期値が与えられる。

式を成立させるために値の変更が必要な変数の数を答えよ。

解法

式を前から順に見て、成立しない節があればその節のどちらかの値を変更し、再度式を先頭から見ればよい。
変更可能な変数の数は高々10なので、分岐回数は高々2^10。
M<=10^5だが、(10^5)*(2^10)なら何とか間に合う。

int N,M;
pair<int,int> L[100001];
string C;
string A;
int md=11;

vector<string> split(const string &str, char delim){
	vector<string> res;
	size_t current = 0, found;
	while((found = str.find_first_of(delim, current)) != string::npos){
		res.push_back(string(str, current, found - current));
		current = found + 1;
	}
	res.push_back(string(str, current, str.size() - current));
	return res;
}

pair<int,int> sp1(string ss) {
	ss=ss.substr(1,ss.size()-2); // del par
	vector<string> Cs=split(ss,'v');
	pair<int,int> p;
	
	if(Cs[0][0]=='~') p.first=-1*atoi(Cs[0].c_str()+1);
	else p.first=atoi(Cs[0].c_str());
	if(Cs[1][0]=='~') p.second=-1*atoi(Cs[1].c_str()+1);
	else p.second=atoi(Cs[1].c_str());
	
	return p;
}

void go(int depth) {
	int i;
	if(depth>=md) return;
	
	FOR(i,M) {
		int lv=A[abs(L[i].first)-1],lpv=lv;
		int rv=A[abs(L[i].second)-1],rpv=rv;
		if(L[i].first<0) lv^=1;
		if(L[i].second<0) rv^=1;
		
		if(lv==0 && rv==0) {
			A[abs(L[i].first)-1]^=1;
			go(depth+1);
			A[abs(L[i].first)-1]=lpv;
			A[abs(L[i].second)-1]^=1;
			go(depth+1);
			A[abs(L[i].second)-1]=rpv;
			return;
		}
	}
	md=min(md,depth);
}

void solve() {
	int f,i,j,k,l,x,y;
	
	cin>>N>>M;
	cin>>C;
	cin>>A;
	
	FOR(i,N) A[i]=(A[i]=='T');
	
	vector<string> Cs=split(C,'^');
	FOR(i,M) L[i]=sp1(Cs[i]);
	go(0);
	
	if(md>=11) _P("TOO LARGE\n");
	else _P("%d\n",md);
}

まとめ

1000回ぐらい式をたどると10^8なのでTLEするかと思ったら意外と間に合うのね。
各変数が絡む節だけ先にくくりだすと早くなったりするのかな？