BOJ 30866 NOT a SAT problem

문제 링크입니다.

문제 요약

주어진 CNF의 결과를 거짓으로 만드세요.

풀이

하나의 OR절만 거짓으로 만들 수 있으면 됩니다. 각 절을 독립적인 문제라고 생각하고 해결해 가며, 한 번이라도 거짓으로 만들 수 있는 절이 확인되면 YES를 출력하고 그대로 프로그램을 종료해 버립시다.

$x_i \vee \lnot x_i$가 어떤 절에 포함되어 있는 경우 그 절은 변수의 값을 어떻게 설정해도 참이 나옵니다. 반대로 각 논리 변수가 최대 하나씩 들어있는 (비어있지 않은) 절이라면, 각 변수의 값을 그 절에서 요구하는 것과 반대로 쥐어주면 그 절을 거짓으로 만들어 전체 CNF를 거짓으로 만들 수 있습니다. 나머지 변수는 아무거나 적당히 주면 됩니다.

길이가 $k$인 절의 거짓화 가능성 판정이 ${\cal O}(k)$에 가능하므로 문제를 ${\cal O}(\Sigma k)$에 해결할 수 있습니다.

코드

#include<bits/stdc++.h>
using namespace std;
using ll = long long;
using pll = pair<ll, ll>;

bool ans[505050], vis[505050];
int in[505050];

int main(){
	cin.tie(0); cout.tie(0); ios::sync_with_stdio(false);
	int n, m; cin >> n >> m;
	while(m--){
		int k; cin >> k;
		for(int i = 0; i < k; i++) cin >> in[i];
		bool flag = 1;
		for(int i = 0; i < k; i++){
			if(vis[abs(in[i])] && ((in[i] > 0) != ans[abs(in[i])])){
				flag = 0; break;
			}
			vis[abs(in[i])] = 1;
			if(in[i] > 0) ans[in[i]] = 1;
		}
		if(flag){
			cout << "YES\n";
			for(int i = 1; i <= n; i++) cout << !ans[i] << ' ';
			return 0;
		}
		for(int i = 0; i < k; i++) ans[abs(in[i])] = vis[abs(in[i])] = 0;
	}
	cout << "NO";
}