3108.txt

北大ACM题目例程 详细的解答过程 程序实现 算法分析

Source

Problem Id:3108  User Id:fzk 
Memory:1024K  Time:410MS
Language:C++  Result:Accepted

Source 

#include <stdio.h>
#include <memory.h>
#include <string>
#include <map>
#include <vector>

using namespace std;


struct HornClause {
	int false_var;
	int dest;
}hc[11000];
vector< HornClause* > e[11000];
int q[11000], qh, qe, hn;
bool sign[11000];

map<string, int> m;
vector<int> var;

int get( char *name ) {
	int t;
	map< string, int >::iterator iter = m.find( name );

	if( iter != m.end() )
		return iter->second;
	else {
		t = m.size();
		e[t].clear();
		m.insert( make_pair( string(name), t ) );
		return t;
	}
}
char name[20010];
void parse( char *w ) {

	int t, i;
	bool key;

	do{
		key = false;
		do {
			w++;
			for( i=0; *w <= 'Z' && *w >= 'A'; i++ )
				name[i] = *w++;
			if( i == 0 )
				var.push_back( 1 );
			else {
				name[i] = '\0';
				var.push_back( get( name ) );
			}
		}while( *w == '&' );

		w++;
		w++;
		for( i=0; *w <= 'Z' && *w >= 'A'; i++ )
			name[i] = *w++;

		if( i == 0 )
			t = 0;
		else {
			name[i] = '\0';
			t = get( name );
		}
		
		
		hc[hn].false_var = var.size();
		hc[hn].dest = t;
		for( i=0; i<var.size(); i++ )
			e[var[i]].push_back( &hc[hn] );
		hn++;
		var.clear( );

		w++;
	}while( *w++ == '&' );

	return;
}

char w[20010];

bool init( ) {

	if( scanf( "%s", w ) == EOF )
		return false;

	m.clear( );
	m.insert( make_pair(string("0"), 0) );
	m.insert( make_pair(string("1"), 1) );
	e[0].clear( );
	e[1].clear( );

	qh = qe = 0;
	q[qe++] = 1;

	memset( sign, 0, sizeof sign );
	sign[1] = true;

	hn = 0;

	parse( w );

	return true;
}

void doit( ) {
	int i, t; 
	bool ans;
	
	ans = true;
		
	while( qh < qe && ans ) {
		t = q[qh++];
		for( i=0; i<e[t].size(); i++ ) {
			
			HornClause *p = e[t][i];
			p->false_var--;

			if( p->false_var == 0 && !sign[ p->dest ] ) {
				if( p->dest == 0 ) {
					ans = false;
					break;
				}
				q[qe++] = p->dest;
				sign[ p->dest ] = true;
			}
		}
	}

	if( !ans )
		printf( "unsatisfiable\n" );
	else {
		bool first = false;
		for( map<string,int>::iterator it=m.begin(); it != m.end(); it++ ) {
			if( it->second > 1 ) {
				if( first )
					printf( "," );
				first = true;
				printf( "%s=%s", it->first.c_str(), sign[ it->second ]?"true":"false" );
			}
		}
		printf( "\n" );
	}
}

int main( ) {
	
	while( init() )
		doit( );

	return 0;
}