2-SAT

2-satisfiability
Boolean satisfiability problem 중에서, 식이 2-CNF 형태로 주어지는 경우를 2-satisfiablity, 줄여서 2-SAT라고 부른다.
k-SAT들 중에서 2-SAT만 따로 빼서 특별하게 설명하는 이유는, 2-SAT 까지만 쉽게 풀리기 때문이다.
- 1-SAT는 자명하고, 3이상의 k-SAT들은 NP-complete이다. 사실 3이상의 k-SAT들은 3-SAT로 리덕션이 되기 때문에 따로 언급할 필요가 없고, 3-SAT는 계산이론쪽에서는 매우 중요하게 다루어진다 (ps쪽에서 2-SAT을 중요하게 다루는것 이상으로..)
- 좀더 엄밀하게는, 2-SAT, Horn-SAT, XOR-SAT 형태만이 다항시간에 풀리는 SAT문제라고 한다..
참고

2-CNF로 표현

교환법칙, 분배법칙 등등을 이용해서 다른 형태들을 x or y 형태로 바꿔줄수 있다.
x == True ⇔ (x or x)
x → y ⇔ (~x or y)
x == y ⇔ (x or ~y) and (~x or y)
x != y ⇔ x == ~y ⇔ (x or y) and (~x or ~y)

At-Most-One

n개의 변수중 최대 1개가 True인 조건을 표현하는 방법.
이것을 CNF로 표현하는 효율적인 방법들에 대한 링크가 많이 있어서 한참 찾아봤었는데, 나중에 알고보니 2-SAT이 아니라 일반적인 SAT에서 가능한 표현방법들도 섞여있었다. 삽질하고 있었음; 그냥 아래 두가지 방법만 기억하자
naive한 방법 - O(n^2)
- 어떤 변수 두개를 골라도, 2개가 모두 True 인 경우가 생기면 안된다. 따라서 모든 (xi, xj) 페어에 대해서 (~xi or ~xj)식을 만족시켜야 한다.
- 변수가 3개 (x,y,z)라면 (~x or ~y) and (~x or ~z) and (~y or ~z) 으로 쓸수 있다.
- 총 O(n^2)개의 절이 추가되므로 시간복잡도도 O(n^2)이 된다
- 대충 변수 5~6개정도까지는 이 방식이 더 효율적일것 같다.
효율적 방법 - O(n)
- 더미변수 y_1,..y_n을 추가한다음 x_1 → y_1, y_i → y_(i+1), x_i → ~y_(i+1) 을 추가한다. O(n)개의 변수와 절을 추가해서 O(n)에 해결 가능
- 이 설명은 https://www.secmem.org/blog/2021/09/01/2sat-app/ 에서 가져온 것이지만, 처음에는 동작 원리가 잘 이해가 안갔다; x_i가 True면, 모든 j>i 에 대해 x_j는 False라는 조건을 붙여주고 싶은데, 이것을 j>i인 모든 (x_i,x_j) 쌍에 대해서 만드는 대신, y_i = (x_1 or x_2 or … or x_i) 라는 변수를 만들어서 처리한 것이다. 그래프로 그려보면 이해가 쉽다.
관련문제:
- TV Show Game - O(n^2) 방법으로 충분
- 19703 - O(n) 방법이 필요
최대 1개 조건 대신, 정확히 1개만 True인 조건은 어떻게 표현하냐고?
- 그거는 최대 1개 조건과 최소 1개 조건을 AND하기만 하면 될것 같지만… n개중 최소 1개 = (x1 or x2 or … or xn) = n-sat이다. 2-sat으로 표현 불가.

알고리즘

그래프로 모델링한 다음에 강한 연결 요소 (Strongly Connected Component / SCC) 를 이용해서 푸는 방법이 가장 대표적이고, 간단하다. 시간복잡도는 O({변수의 갯수} + {2-CNF식의 절의 갯수})
- 2-SAT을 linear time에 풀 수 있는 알고리즘은 이 외에도 더 있다는 것 같지만, 어떤 알고리즘이 있는지 들어본 적은 없다. 그냥 2-SAT은 SCC로 푼다고 알고 있으면 될듯. 백준에서도 2-sat 태그가 달린 문제에는 SCC 태그도 항상 같이 달려있고, 단계별로 풀어보기에서도 SCC 안에 2-sat 문제들을 같이 포함시켜놨다.
해가 존재하는 지를 확인하는 방법은..
- 먼저 주어진 변수들 x1,x2,…과 니게이션된 변수들 ~x1, ~x2, …을 노드로 하는 그래프를 만든다. (x_i V x_j)의 절마다 ~x_i→x_j, ~x_j→x_i 의 두개의 엣지를 만든다.
- 이제, 그래프를 SCC들로 분할한다. 어떤 x_i와 ~x_i 노드가 같은 SCC에 속하는 경우가 있다면, 이 2-sat 문제는 해가 없다. 역으로, x_i와 ~x_i 가 같은 SCC에 속하는 경우가 없다면, 2-sat 문제에는 해가 존재한다
해가 존재할때, 그중 한개의 해를 구하기 위해서는 condensation graph에서 위상정렬을 거쳐서 구할 수 있다.
- x_i와 ~x_i 중에서 더 위상정렬순서상으로 더 앞쪽에 오는 쪽을 False로 처리하면 된다. 다시 말해, x_i ⇒ ~x_i 의 경로가 있으면 x_i값을 False로, ~x_i ⇒ x_i 의 경로가 있으면 x_i값을 True로 주면 된다.
  - x_i ⇔ ~x_i 처럼 양쪽으로 경로가 다 존재하는 경우가 있다면, 앞에서 말한것처럼 해가 없는 문제이다.
- 사실 SCC를 구하는 과정에서 SCC가 위상순으로 정렬되기 때문에, 매우 심플한 코드로 구현가능하다.

구현/설계 이슈

처음에는 2-CNF 형태의 문제를 받아서 결과를 돌려주는 함수로 만들려고 했다.
- 인자로 받을 2-CNF는 list[tuple[int, int]] 형태로 받는다. 각 튜플 하나가 (x or y)형태의 절에 해당된다.
- x와 ~x 를 어떻게 구분해서 받을 것인가…
  - 문제들 중에서는 x_i를 i, ~x_i를 -i로 입력받는 형태가 가장 흔하다. 이렇게 +와 -부호를 통해서 negation을 표현해서 인자로 전달할수 있으면 입력데이터를 처리하기가 가장 간단하기는 하다. 게다가 파이썬에서는 음수 인덱싱을 지원하기때문에, 내부 graph 표현에서도 그대로 이값을 저장해서 SCC를 돌리고 하는 것도 가능하긴 하다.
    - 그러나 이경우에는 0을 사용할수 없다. 모든 입력을 0-based로 바꿔서 처리한다는 기본 규칙과 어긋난다. 그리고 내부 그래프 표현에서도 음수를 그대로 사용하는 것은 다른 그래프 알고리즘들과 호환이 안될수도 있다.
  - x_i, ~x_i 를 (0, -1), (1,-2), … 과 같은 식으로 사용하는 방법도 있다. 0-based라서 조금더 일관성이 있고, neg 표현도 비트 neg 연산자 ~을 그대로 사용해서 처리할수 있다는 장점이 있다. 하지만 문제에서 입력으로 주는 값들과 포맷이 달라지기 때문에 처리가 필요하고, ~를 붙이는 것이 덜 직관적이기도 하다. (관점에 따라서는 더 직관적일수도..)
  - x_i, ~x_i 를 i*2와 i*2+1 로 처리하는 방법. neg연산은 x^1 로 처리된다. 0-based이고 음수를 쓰지 않아서 내부적으로 좋긴 하다..
  - 이 외에도 여러가지 방법이야 있겠지만.. 일단 내부적으로는 음수를 쓰지 말고, [0,2n) 범위로 다 바꿔서 쓰기로 결정했다. [x1, ~x1, x2, ~x2, …] 순서로 저장한다. 외부에서 인자로 전달할때는 0-based index와 ~를 이용해서 전달하기로 했다.
    - 예를들어 x_3과 ~x_3은 인자로 넘길때는 2과 ~2 (=-3)으로 전달되고, 내부에서는 2*2와 2*2+1 의 인덱스에 저장된다.
- 리턴값은? 해가 있는지 여부만 궁금할때와, 실제 해가 궁금할때?
  - 해가 있는지 여부만 궁금할때가 더 많긴 하지만, 실제 해가 궁금할때도 있다. 함수를 따로 분리하지 않는 이상, 더 포괄적인 답인 실제 해를 리턴해야 맞을거 같은데, 이렇게 한다면 해가 없을 경우에는 예외를 발생시켜야 할지 None를 리턴해야 할지가 고민. 보통은 원하는 답을 얻을수 없을 경우에는 예외를 발생시키는 것이 맞는데.. (예를들어, 최단거리를 리턴하는 벨만포드 알고리즘에서, 음수 사이클이 발견된다면 None을 리턴하는게 아니라 예외를 날리는게 더 적절하다.) 근데 문제는 해의 존재여부만 궁금한 경우가 훨씬 더 많다는 것. 고민끝에 None를 리턴하는걸로 결정했다.
그러나 함수로 만드는데에 심각한 문제를 발견.. 클래스로 다시 만들기로 했다.
- 함수형태의 API는 먼제 문제로부터 2-CNF를 만들어서 함수로 전달하면, 함수내에서 2-CNF를 다시 그래프로 바꾸어서 SCC를 돌리게 된다. 이 과정에서 속도 저하도 당연히 발생하긴 하지만, 그것은 그냥 감수해야 하는 부분이라고 생각했었다.. 그러나 15675 에서 감수하는 것이 불가능한 문제 - 메모리 초과 이슈를 겪었다. list[tuple[int,int]] 타입의 2-CNF를 만드는 것을 생략하고 바로 graph를 건드려야만 해결이 가능했고, 내부적으로 graph를 멤버로 갖는 클래스 형태로 라이브러리를 만들기로 했다.
- 기왕 클래스로 만드는 김에, 멤버함수도 좀더 여러개를 갖도록 했다.
  - 위에서 어떻게 처리할지 고민했던, 해의 존재여부와 실제 해를 찾는 함수를 그냥 분리해서 제공하기로 했다.
    - 함수이름은 좀더 직관적인 has_answer/get_answer 과 좀더 포멀한 is_satisfiable/find_truth_assignment 중 후자를 사용하기로 결정.
  - 하나의 (x or y) 절을 추가하는 함수 뿐만 아니라, x==y 절 (실제로는 (x or ~y) and (~x or y)로 해석되는..) 을 추가하는 함수도 같이 만들었다.
- 클래스 이름은? TwoSat vs TwoSatisfiablity? ⇒ TwoSat으로 결정.
- 모듈도 graph에 넣는 대신 twosat으로 따로 만들기로 했다.
  - 코드에서는 two_sat = twosat.TwoSat(n) 으로 써야 할텐데 twosat이 너무 많이 들어가나 싶기도하지만.. 익숙해지면 괜찮을듯.

코드

teflib.twosat.TwoSat

벤치마크

가위바위보 N=10,000, M=10,000, Satisfiability만 체크
2-SAT - 3 N=10,000, M=100,000, Satisfiability만 체크
2-SAT - 4 N=10,000, M=100,000, 실제 해를 출력

해결 불가 문제

2416 N=500,000, M=250,000 인데. 메모리 초과가 난다 (128MB 제한)
20942 N=250,000, M=500,000 인데, 시간 초과가 난다 (추가시간없는 1초 제한)
8310 N=1,000,000, M>=1,000,000 인데, 시간 초과가 난다 (3초 제한, C++로도 2초 이상 걸림)

확장

3-sat 문제는 NP-complete 이다.
일반적인 sat 문제는 3-sat로 변환이 가능하다. (NP-complete)
2-sat 외에 Polynomial time에 풀릴수 있는 다른 sat 문제는 Horn-satisfiability라고 한다. 하나의 절 안에 최대 1개의 positive literal만 있어야 하고 나머지는 negative literal들로 구성된 형태이다.
그 외에도, 위키피디아의 https://en.wikipedia.org/wiki/2-satisfiability#Complexity_and_extensions에 보면 연관된 문제들이 많이 나와있는데, 재미있는 것들 몇개를 추리면
- 조건을 만족하는 assignment의 갯수를 찾기 (#2SAT) 는 #P-complete
- 주어진 절들중 최대한 많은 갯수를 만족시키는 assignment를 찾기 (MAX-2-SAT) 는 NP-hard
- k개의 변수를 True로 하는 assignment를 찾기 (W2SAT) 는 NP-complete

목차

2-SAT

2-CNF로 표현

At-Most-One

알고리즘

구현/설계 이슈

코드

벤치마크

해결 불가 문제

확장