[Python] 11277번 2-SAT - 1 / 11278번 2-SAT - 2

https://www.acmicpc.net/problem/11277

11277번: 2-SAT - 1

https://www.acmicpc.net/problem/11278

11278번: 2-SAT - 2

---

 

22/09/28

 

 

두 문제가 거의 유사하고, 첫 번째 문제에서 코드 한 줄만 추가하면 두 번째 문제를 해결할 수 있으므로 같이 작성한다.

 

2-SAT 알고리즘을 전혀 사용하지 않고도 풀 수 있는 단순 브루트 포스 문제로, 전형적인 "문제 해석하는 것이 더 어려운 문제"이다.

---

 

문제 접근 방식:

 

 

한국말이지만 정말 해석하기 어려운 이 문제를 보자.

 

이 문제의 목적은 다음과 같다.

 

어떤 논리 식이 주어지면, 그 식의 변수들 각각에 True 또는 False의 값을 대입 함으로써, 그 식 전체를 True로 만들 수 있느냐를 판단하는 것.

 

먼저, 이 문제에서 주어진 논리 식에 대한 종류와 그 논리식을 구성할 때 사용되는 연산들의 종류에 대해서 알아야 한다.

 

먼저, ∨는 OR를, ∧는 AND, ¬은 NOT을 나타낸다.

 

잘 알다시피, OR연산은 둘 중 하나가 True면 True의 값을 내보내는 연산, AND연산은 둘 중 하나가 False면 False의 값을 내보내는 연산, NOT연산은 True면 False, False면 True를 내보내는 연산이다.

 

예시로, 어떤 두 불리언 변수(이 변수에 True나 False의 값을 대입한다)가 주어져 있다고 해보자.

x1이라는 변수와 x2라는 변수에 OR연산을 취해주었다고 한다면, 이는 x1 ∨ x2와 같이 쓸 수 있다.

 

물론, 이 x1 ∨ x2의 진리 값은 x1과 x2에 어떤 값을 넣어주냐에 따라서 다르다.

 

만약 x1에 False, x2에 False를 대입했다면, 위 식의 값은 False가 될 것이다.

하지만 둘 중 하나에라도 True값을 대입했다면, 위 식의 값은 True가 될 것이다.

 

여기서 하나의 개념을 정의할 것이다. 이것은 절(Clause)라고 불리는 것인데, 이는 한 개 이상의 불리언 변수를 OR연산을 통해 괄호로 묶은 것을 의미한다.

 

위에서의 (x1 ∨ x2) 또한, 하나의 절이라고 생각할 수 있다.

 

이러한 절들을 AND연산을 통해 여러 개 묶으면, 이를 Conjunctive Normal Form, 줄여서 CNF라고 부른다.

 

2-CNF식은 AND연산을 통해 묶인 모든 절들이 2개의 불리언 변수로 이루어져있다.

 

자. 이제 다시 되돌아가서, 우리의 목표를 되짚어보면, 어떤 2-CNF식이 주어져 있을 때, 그 식이 True가 될 수 있냐를 판단하는 것이다.

 

불리언 변수의 개수가 N 개라고 해보자.

그러면, 대입할 수 있는 모든 경우의 수는 [True, True, ..., True](N개) 부터 [False, False, ..., False]까지 총 2^N개가 된다.

 

변수 개수의 범위는 최대 20까지 이므로, 2^20 = 약 100만 정도 된다.

 

때문에 충분히 대입할 수 있는 모든 경우의 수를 대입해 가며 가능한지 판단하면 된다.

 

itertools의 product함수를 사용하여 대입할 수 있는 모든 경우의 수를 구현하였다.

---

아래는 내가 위의 접근 방식과 같이 작성한 파이썬 코드이다. 더보기를 누르면 확인할 수 있다.

# 11277번 2-SAT - 1
# 구현, 브루트 포스
'''
접근 방법:
변수의 개수가 20개 이므로 2^20 = 대략 100만 정도이고
절의 개수가 100개 이므로
100만 * 100 = 1억이므로
충분히 1초내로 돌릴 수 있다.
'''
import sys
from itertools import *
input = sys.stdin.readline

N, M = map(int, input().rstrip().split())
boolean = [0, 1]
CNF = [list(map(int, input().rstrip().split())) for _ in range(M)]
for bools in product(boolean, repeat=N):
    is_ok = True
    for i, j in CNF:
        xi, xj = bools[abs(i)-1], bools[abs(j)-1]
        if i < 0:
            xi = not xi
        if j < 0:
            xj = not xj
        if not (xi or xj):
            is_ok = False
            break
    if is_ok:
        print(1)
        break
else:
    print(0)

# 11278번 2-SAT - 2
# 구현, 브루트 포스
'''
접근 방법:
변수의 개수가 20개 이므로 2^20 = 대략 100만 정도이고
절의 개수가 100개 이므로
100만 * 100 = 1억이므로
충분히 1초내로 돌릴 수 있다.
'''
import sys
from itertools import *
input = sys.stdin.readline

N, M = map(int, input().rstrip().split())
boolean = [0, 1]
CNF = [list(map(int, input().rstrip().split())) for _ in range(M)]
for bools in product(boolean, repeat=N):
    is_ok = True
    for i, j in CNF:
        xi, xj = bools[abs(i)-1], bools[abs(j)-1]
        if i < 0:
            xi = not xi
        if j < 0:
            xj = not xj
        if not (xi or xj):
            is_ok = False
            break
    if is_ok:
        print(1)
        print(*bools)
        break
else:
    print(0)