절 세기

매년 열리는 3-SAT 대회가 열렸다. 참가자들은 제한 시간 안에 최대한 많은 3-SAT 인스턴스를 해결하기 위해 경쟁한다. 3-SAT는 대표적인 NP-완전 문제로, 논리곱 표준형으로 주어진 불리언 식이 주어진다. 이 식은 정확히 세 개의 리터럴로 이루어진 절들의 집합이다. 각 리터럴은 변수를 긍정 또는 부정으로 가리키며, 변수는 True 또는 False 중 하나의 값을 가진다. 문제는 모든 절이 True로 평가되도록 변수에 값을 할당하는 방법이 존재하는지 여부이다. 어떤 절에도 같은 리터럴이 중복으로 들어가지 않는다. 단, 한 절에 ¬xi와 xi가 동시에 들어가는 것은 가능하다. 아래는 3-SAT 인스턴스의 예시이다(예제 입력 1에서 가져옴).

(¬x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2 ∨ x3) ∧ (x1 ∨ ¬x2 ∨ x3) ∧ (x1 ∨ ¬x2 ∨ ¬x3) ∧ (x1 ∨ x2 ∨ ¬x3)

Øyvind는 이 대회의 심사위원으로, 대회가 시작되기 전에 다른 심사위원들이 만든 문제 인스턴스의 품질을 검증하는 일을 맡는다. Øyvind는 절이 여덟 개 미만인 3-SAT 인스턴스를 싫어한다. 이런 인스턴스는 항상 만족 가능하므로 참가자들에게 실질적인 도전이 되지 않기 때문이다. 따라서 그는 이런 문제 인스턴스를 불만족스럽다고 판단한다. 절이 여덟 개 이상인 인스턴스를 만나면, Øyvind는 그 인스턴스가 만족 가능한지 알아내는 것이 진짜 도전이라는 것을 안다. 그래서 그는 이런 문제 인스턴스를 만족스럽다고 판단한다. 3-SAT 인스턴스가 주어졌을 때, Øyvind의 판단을 대신 내려줄 수 있는가?

입력은 3-SAT 문제의 인스턴스 하나이다. 첫째 줄에는 공백으로 구분된 두 정수 m (1 ≤ m ≤ 20)과 n (3 ≤ n ≤ 20)이 주어진다. m은 절의 수, n은 변수의 수이다. 그 다음 m개의 절이 한 줄에 하나씩 이어진다. 각 절은 [−n, n] \ {0} 범위의 서로 다른 세 정수로 이루어지며 공백으로 구분된다. 각 절에서 세 값은 그 절의 세 리터럴에 대응한다. 리터럴이 음수이면 해당 변수가 False일 때 그 절이 만족됨을 뜻하고, 양수이면 해당 변수가 True일 때 그 절이 만족됨을 뜻한다.

Øyvind가 그 3-SAT 인스턴스를 만족스럽다고 판단하면 한 줄에 “satisfactory”를, 그렇지 않으면 “unsatisfactory”를 출력한다.