diff --git a/README.md b/README.md index 8a35ef5..93fc634 100644 --- a/README.md +++ b/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 ``` diff --git a/README_ja.md b/README_ja.md index 098f6dc..89f4d32 100644 --- a/README_ja.md +++ b/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 - ## インストール ``` diff --git a/atcoder/twosat.py b/atcoder/twosat.py new file mode 100644 index 0000000..1f2c1dc --- /dev/null +++ b/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 diff --git a/example/twosat_practice.py b/example/twosat_practice.py new file mode 100644 index 0000000..0bbbf94 --- /dev/null +++ b/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()