Turf Wars

• 각 영역을 boolean 변수로 만들자. 변수의 값은 그 영역을 포기하면 True가 되고, 포기 안하면 False를 갖도록 하자.
• 이제 변수들간의 관계를 2-SAT으로 모델링할수 있다.
• 영역 x와 영역 y가 겹친다면, 둘중 한개 이상은 포기되어야 한다 ⇒ 이것은 그냥 x or y 로 표현할수 있다.
• 같은 갱에 속한 영역들 중에서는 최대 한개만 true가 될수 있다 ⇒ 이것은 at-most-one 조건으로 표현하면 된다.
• 이렇게 모델링한 다음, 2-sat이 해를 갖는지 여부만 확인하면 된다. O(N*M)개의 변수와 O((N*M)^2)개의 절을 갖는 CNF로 표현되므로 총 시간복잡도는 O((N*M)^2).

(다이아몬드 이상은 코드 첨부 생략)

• Dependency: teflib.twosat.TwoSat