[BOJ] 11278 2-SAT 2

SAT 관련해서 찾아보니 막막해서 참고없이 정석대로 풀기는 포기하였습니다. 

시간제한은 무려 2초, 만들 수 있는 x1,x2...xi의 배열의 최대 길이는 n번째 위치에 있는 xn이 가질수 있는 값은 2개 (0,1) 최대 크기 20인 배열의 경우의 수 2**20 = 약 100만개의 배열이 존재, 검사해야할 쌍(a,b)의 최대 개수는 100개 100만개의 배열에 100개의 쌍을 대입해서 비교하고 도중에 틀린 값이 있으면 더이상 비교를 진행하지 않으면 100*100만 1억번 안쪽으로 가능할 것이라 생각했습니다.

배열은 오직 0과 1만 가질수 있으므로 경우의 수에 해당하는 배열 만들기는 매우 간단했습니다.

def make(word):
    if len(word)==n+1:
        sat(word)
        return
    for i in range(2):
        make(word+[i])

기존 배열에 [0] 또는 [1]을 붙이며 재귀하다가 길이가 n+1 (맨 처음 배열에 의미없는 값을 하나 넣어줘서 인덱스를 맞춰주었기 때문에..)이라면 입력받았던 절들을 넣어서 맞는지 확인해주었습니다.

다음은 sat 함수입니다.

def sat(to_check):
    for xi,xj in jul:
        jul1=to_check[xi] if xi>0 else not to_check[-xi]
        jul2=to_check[xj] if xj>0 else not to_check[-xj]
        if (jul1 or jul2)==0:
            return
    print(1)
    for i in range(1,n+1):
        print(to_check[i],end=' ')
    exit()

체크할 배열을 전달받고 저장해논 절들을 넣어주며 비교했습니다. 만약 둘다 0, 0 이라면 해당 절의 값은 False가 되므로 나중에 or연산에 의해 무조건 결과값이 False가 됩니다. 그러므로 0,0인 경우 함수를 종료시켜주었습니다.

만약 모든 절의 값들을 만족시킨 경우 1을 출력하고 전달받은 배열안에 들어있는 값들을 출력해준 다음 exit()로 프로그램을 종료시켜 그 이후 스크립트는 실행되지 않도록 해주었습니다.

아래는 최종 코드입니다.

 

from sys import stdin
input=stdin.readline

n,m=map(int,input().split())
jul=[]

for i in range(m):
    a,b=map(int,input().split())
    jul.append((a,b))

def make(word):
    if len(word)==n+1:
        sat(word)
        return
    for i in range(2):
        make(word+[i])

def sat(to_check):
    for xi,xj in jul:
        jul1=to_check[xi] if xi>0 else not to_check[-xi]
        jul2=to_check[xj] if xj>0 else not to_check[-xj]
        if (jul1 or jul2)==0:
            return
    print(1)
    for i in range(1,n+1):
        print(to_check[i],end=' ')
    exit()

make([''])
print(0)

make에 맨 처음에 아무의미없는 값을 하나 넣어주어서 인덱스를 맞춰주었고, 만약 make함수가 다 돌아가며 exit이 실행되지 않는다면 맨 마지막 줄의 print(0)이 실행됩니다.

n과 m이 매우 작기에 가능한 풀이였고 솔직히 제출하면서도 시간초과를 생각하고있었는데 왜 맞는지 모르겠었습니다.. 당연히 11277 2-sat 1은 시간제한이 1초라 안될 줄 알았는데도 되서 놀라웠습니다 ㅋㅋ