Port two SAT

README.md

@@ -26,6 +26,7 @@ ac-library-python is a Python port of [AtCoder Library (ACL)](https://atcoder.jp
 + maxflow
 + mincostflow
 + scc
++ twosat
 
 ### Work in progress
 
@@ -40,10 +41,6 @@ ac-library-python is a Python port of [AtCoder Library (ACL)](https://atcoder.jp
 + convolution
 + modint
 
-#### Graph
-
-+ twosat
-
 ## Install
 
 ```

README_ja.md

@@ -24,6 +24,7 @@ ac-library-pythonは、[AtCoder Library (ACL)](https://atcoder.jp/posts/517)のP
 + maxflow
 + mincostflow
 + scc
++ twosat
 
 ### 準備中
 
@@ -38,10 +39,6 @@ ac-library-pythonは、[AtCoder Library (ACL)](https://atcoder.jp/posts/517)のP
 + convolution
 + modint
 
-#### グラフ
-
-+ twosat
-
 ## インストール
 
 ```

atcoder/twosat.py

@@ -0,0 +1,35 @@
+import typing
+
+import atcoder._scc
+
+
+class TwoSAT:
+    '''
+    Reference:
+    B. Aspvall, M. Plass, and R. Tarjan,
+    A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean
+    Formulas
+    '''
+
+    def __init__(self, n: int = 0) -> None:
+        self._n = n
+        self._answer = [False] * n
+        self._scc = atcoder._scc.SCCGraph(2 * n)
+
+    def add_clause(self, i: int, f: bool, j: int, g: bool) -> None:
+        assert 0 <= i < self._n
+        assert 0 <= j < self._n
+
+        self._scc.add_edge(2 * i + (0 if f else 1), 2 * j + (1 if g else 0))
+        self._scc.add_edge(2 * j + (0 if g else 1), 2 * i + (1 if f else 0))
+
+    def satisfiable(self) -> bool:
+        scc_id = self._scc.scc_ids()[1]
+        for i in range(self._n):
+            if scc_id[2 * i] == scc_id[2 * i + 1]:
+                return False
+            self._answer[i] = scc_id[2 * i] < scc_id[2 * i + 1]
+        return True
+
+    def answer(self) -> typing.List[bool]:
+        return self._answer

example/twosat_practice.py

@@ -0,0 +1,41 @@
+# https://atcoder.jp/contests/practice2/tasks/practice2_h
+
+import sys
+
+from atcoder.twosat import TwoSAT
+
+
+def main() -> None:
+    n, d = map(int, sys.stdin.readline().split())
+    x = [0] * n
+    y = [0] * n
+    for i in range(n):
+        x[i], y[i] = map(int, sys.stdin.readline().split())
+
+    two_sat = TwoSAT(n)
+
+    for i in range(n):
+        for j in range(i + 1, n):
+            if abs(x[i] - x[j]) < d:
+                two_sat.add_clause(i, False, j, False)
+            if abs(x[i] - y[j]) < d:
+                two_sat.add_clause(i, False, j, True)
+            if abs(y[i] - x[j]) < d:
+                two_sat.add_clause(i, True, j, False)
+            if abs(y[i] - y[j]) < d:
+                two_sat.add_clause(i, True, j, True)
+
+    if not two_sat.satisfiable():
+        print("No")
+    else:
+        print("Yes")
+        answer = two_sat.answer()
+        for i in range(n):
+            if answer[i]:
+                print(x[i])
+            else:
+                print(y[i])
+
+
+if __name__ == '__main__':
+    main()