수정된 SAT

불리언 만족성 문제(SAT)는 논리곱 정규형으로 주어진 불리언 식에 대해, 식 전체가 참이 되도록 각 변수에 참 또는 거짓을 할당하는 방법이 존재하는지 판정하는 문제이다.

논리곱 정규형에서 식은 정해진 형식으로 주어진다. 사용되는 논리 연산은 논리곱, 논리합, 부정뿐이며 각각 $\wedge$, $\vee$, $\neg$로 나타낸다. 식은 절이라 부르는 여러 부분 $C_1, \dots, C_m$의 논리곱으로 이루어진다. 즉 식 $\phi$는 다음과 같은 형태이다.

$\phi = C_1 \wedge \cdots \wedge C_m.$

각 절도 정해진 형식을 갖는다. 각 절은 변수 또는 변수의 부정인 리터럴들의 논리합을 괄호로 묶은 것이다. 따라서 $(x_1 \vee \neg x_2)$는 올바른 절이지만, $(x_1 \wedge \neg x_2)$는 논리곱 연산을 사용하므로 올바른 절이 아니다. 완전한 식의 예는 다음과 같다.

$\phi = (x_1 \vee x_2 \vee x_3) \wedge (\neg x_1) \wedge (x_1 \vee \neg x_2 \vee x_3) \wedge (x_2 \vee \neg x_3).$

SAT의 변형으로 각 절이 최대 $k$개의 리터럴을 갖는 k-SAT이 있다. 위 식은 3-SAT의 예이지만 2-SAT의 예는 아니다. 이 문제들에서 식이 참이 되려면 모든 절이 참이어야 하므로, 각 절에서 적어도 하나의 리터럴($x_i$ 또는 $\neg x_i$ 형태)이 참이어야 한다.

할당은 각 변수를 참 또는 거짓으로 정하는 방법이다. 이 문제에서는 3-SAT의 변형을 다루며, 유효한 할당은 각 절에서 참인 리터럴이 정확히 1개 또는 정확히 3개여야 한다. 식이 주어지면 이 추가 제약을 고려하여 유효한 할당이 존재하는지 판정해야 한다. 유효한 할당이 존재하면 사전순으로 가장 큰 할당을 출력해야 한다. 사전순은 다음과 같이 정의된다. 서로 다른 두 할당에 대해 두 할당에서 값이 다른 가장 작은 번호의 변수를 비교하며, 그 변수에 참을 할당한 쪽이 더 큰 할당이다.

첫째 줄에 절의 수와 변수의 수를 나타내는 두 정수 $M$, $N$이 주어진다. ($1 \le M, N \le 2000$) 이어서 $M$개의 줄에 각각 하나의 절이 주어진다(형식은 예제를 참고). 연속한 절은 문자열 “ and”로 구분된다. 각 절은 최대 3개의 리터럴을 갖는다. 변수는 “x” 뒤에 1과 $N$ 사이의 수가 붙은 형태로 나타낸다. 연속한 두 공백은 없으며 줄 끝에도 공백이 없다.

첫 번째 예제는 위의 식 $\phi$를 나타낸다.

사전순으로 가장 큰 유효한 할당에 대응하는 $N$개의 문자를 한 줄에 출력하거나, 유효한 할당이 없으면 impossible을 출력한다. $i$번째 문자는 할당에서 $i$번 변수가 참이면 T, 거짓이면 F이다.