AOJ1078:SAT-EN-3

問題

http://judge.u-aizu.ac.jp/onlinejudge/description.jsp?id=1078
佐天さん。

方針

加法標準形のSATなので1clauseでもsatisfiableなら全体としてsatisfiableである。
文字処理が若干めんどくさい。
mapでどの文字リテラルがtrueかfalseのどちらのassignを要求しているかを取っておく。
読み込んだリテラルが既にmapに存在してその要求したboolと違っていたらそのclauseはunsatisfiable。
要はa&~aみたいなのがあったらダメ。当たり前である。
mapはclauseごとにclearする。

以下ソースコード

#include <iostream>
#include <string>
#include <map>
#include <algorithm>
using namespace std;

int main(){
	string str;
	
	while(cin >> str){
		if(str == "#") break;
		bool ret = false;
		bool sable = true;
		map<char,bool> m;
		for(int i=0;i<str.size();i++){
			if(str[i] == '(' || str[i] == '&' || str[i] == ')') continue;
			else if(str[i] == '|'){
				if(sable == true){
					ret = true;
					break;
				}
				sable = true;
				m.clear();
			}else{
				bool tmpb = true;
				char tmpc;
				if(str[i] == '~'){
					tmpb = false;
					i++;
				}
				tmpc = str[i];
				if(m.find(tmpc) != m.end() && m[tmpc] != tmpb){
					sable = false;
				}
				m[tmpc] = tmpb;
			}
		}
		sable?ret=true:ret=false;
		ret?cout<< "yes" << endl:cout << "no" << endl;
	}
}