6100 : 2-SAT 기초 — SCC 활용
•시간제한: 2.000 S
•메모리제한: 256 MB
•제출: 0
•통과: 0
•만든사람: suakii
문제 설명
2-SAT(2-Satisfiability) 문제는 논리 변수와 OR 절(Clause)들의 AND 연산으로 구성된 논리식이 참이 될 수 있는지를 판단하는 문제입니다.
각 절이 (A V B) 형태일 때, 논리 구조인 함의 그래프(Implication Graph) 즉, (~A -> B)와 (~B -> A) 두 방향성 간선으로 변환하고, 강연결요소(SCC)를 추출하여 만족 가능성을 해결하십시오.
어떤 논리 변수 X에 대해 X와 ~X가 동일한 SCC에 속해 있다면, 모순이 발생하여 만족시킬 수 없습니다. 만족 가능할 시 식을 참으로 만드는 각 변수의 참/거짓 값도 결정하여 출력하십시오.
각 절이 (A V B) 형태일 때, 논리 구조인 함의 그래프(Implication Graph) 즉, (~A -> B)와 (~B -> A) 두 방향성 간선으로 변환하고, 강연결요소(SCC)를 추출하여 만족 가능성을 해결하십시오.
어떤 논리 변수 X에 대해 X와 ~X가 동일한 SCC에 속해 있다면, 모순이 발생하여 만족시킬 수 없습니다. 만족 가능할 시 식을 참으로 만드는 각 변수의 참/거짓 값도 결정하여 출력하십시오.
입력 설명
첫째 줄에 변수의 개수 N (1 ≤ N ≤ 10,000)과 절의 개수 M (1 ≤ M ≤ 100,000)이 주어집니다.
둘째 줄부터 M개의 줄에 각 절을 이루는 두 정수 a, b가 주어집니다. (양수 i는 x_i, 음수 -i는 ~x_i를 뜻합니다.)
둘째 줄부터 M개의 줄에 각 절을 이루는 두 정수 a, b가 주어집니다. (양수 i는 x_i, 음수 -i는 ~x_i를 뜻합니다.)
출력 설명
만족시킬 수 없으면
만족시킬 수 있다면 첫째 줄에
NO를 출력합니다.만족시킬 수 있다면 첫째 줄에
YES를 출력하고, 둘째 줄에 x_1부터 x_N까지의 참/거짓 값(1 또는 0)을 공백으로 구분하여 출력합니다.
입력 예시
COPY
복사되었습니다!
복사되었습니다!
3 4
1 2
-2 3
-1 -3
1 3
출력 예시
COPY
복사되었습니다!
복사되었습니다!
YES
0 1 1도움
SCC 위상정렬에서 나중에 완성(코사라주에서는 발견 순서가 작은 것)되는 변수 상태에 참(1)을 부여하는 표준 2-SAT 값 대입 방식을 이용하십시오.
scc_id[x] < scc_id[~x] 인 경우 1, 아닌 경우 0을 부여하면 모순 없이 값을 결정할 수 있습니다.