結果
問題 | No.3031 曲面の向き付け |
ユーザー |
![]() |
提出日時 | 2025-02-21 23:09:42 |
言語 | PyPy3 (7.3.15) |
結果 |
AC
|
実行時間 | 1,956 ms / 2,000 ms |
コード長 | 5,185 bytes |
コンパイル時間 | 294 ms |
コンパイル使用メモリ | 82,352 KB |
実行使用メモリ | 425,220 KB |
最終ジャッジ日時 | 2025-02-21 23:09:56 |
合計ジャッジ時間 | 13,571 ms |
ジャッジサーバーID (参考情報) |
judge1 / judge3 |
(要ログイン)
ファイルパターン | 結果 |
---|---|
sample | AC * 4 |
other | AC * 29 |
ソースコード
import sysimport typingclass CSR:def __init__(self, n: int, edges: typing.List[typing.Tuple[int, int]]) -> None:self.start = [0] * (n + 1)self.elist = [0] * len(edges)for e in edges:self.start[e[0] + 1] += 1for i in range(1, n + 1):self.start[i] += self.start[i - 1]counter = self.start.copy()for e in edges:self.elist[counter[e[0]]] = e[1]counter[e[0]] += 1class SCCGraph:'''Reference:R. Tarjan,Depth-First Search and Linear Graph Algorithms'''def __init__(self, n: int) -> None:self._n = nself._edges: typing.List[typing.Tuple[int, int]] = []def num_vertices(self) -> int:return self._ndef add_edge(self, from_vertex: int, to_vertex: int) -> None:self._edges.append((from_vertex, to_vertex))def scc_ids(self) -> typing.Tuple[int, typing.List[int]]:g = CSR(self._n, self._edges)now_ord = 0group_num = 0visited = []low = [0] * self._norder = [-1] * self._nids = [0] * self._nsys.setrecursionlimit(max(self._n + 1000, sys.getrecursionlimit()))def dfs(v: int) -> None:nonlocal now_ordnonlocal group_numnonlocal visitednonlocal lownonlocal ordernonlocal idslow[v] = now_ordorder[v] = now_ordnow_ord += 1visited.append(v)for i in range(g.start[v], g.start[v + 1]):to = g.elist[i]if order[to] == -1:dfs(to)low[v] = min(low[v], low[to])else:low[v] = min(low[v], order[to])if low[v] == order[v]:while True:u = visited[-1]visited.pop()order[u] = self._nids[u] = group_numif u == v:breakgroup_num += 1for i in range(self._n):if order[i] == -1:dfs(i)for i in range(self._n):ids[i] = group_num - 1 - ids[i]return group_num, idsdef scc(self) -> typing.List[typing.List[int]]:ids = self.scc_ids()group_num = ids[0]counts = [0] * group_numfor x in ids[1]:counts[x] += 1groups: typing.List[typing.List[int]] = [[] for _ in range(group_num)]for i in range(self._n):groups[ids[1][i]].append(i)return groupsclass TwoSAT:'''2-SATReference:B. Aspvall, M. Plass, and R. Tarjan,A Linear-Time Algorithm for Testing the Truth of Certain Quantified BooleanFormulas'''def __init__(self, n: int = 0) -> None:self._n = nself._answer = [False] * nself._scc = SCCGraph(2 * n)def add_clause(self, i: int, f: bool, j: int, g: bool) -> None:assert 0 <= i < self._nassert 0 <= j < self._nself._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 Falseself._answer[i] = scc_id[2 * i] < scc_id[2 * i + 1]return Truedef answer(self) -> typing.List[bool]:return self._answerN = int(input())tri = [tuple(map(int, input().split())) for _ in range(N)]from collections import defaultdictdict = defaultdict(lambda: -1)sat = TwoSAT(N)def make(a, b):return (a << 30) | bfor i in range(N):a, b, c = tri[i]k0 = make(a, b)k1 = make(b, c)k2 = make(a, c)if dict[k0] == -1:dict[k0] = i*2elif dict[k0] == -2:exit(print("NO"))else:x = dict[k0]j = x // 2if x % 2:sat.add_clause(i, True, j, False)sat.add_clause(i, False, j, True)else:sat.add_clause(i, True, j, True)sat.add_clause(i, False, j, False)dict[k0] = -2if dict[k1] == -1:dict[k1] = i*2elif dict[k1] == -2:exit(print("NO"))else:x = dict[k1]j = x // 2if x % 2:sat.add_clause(i, True, j, False)sat.add_clause(i, False, j, True)else:sat.add_clause(i, True, j, True)sat.add_clause(i, False, j, False)dict[k1] = -2if dict[k2] == -1:dict[k2] = i*2+1elif dict[k2] == -2:exit(print("NO"))else:x = dict[k2]j = x // 2if not (x % 2):sat.add_clause(i, True, j, False)sat.add_clause(i, False, j, True)else:sat.add_clause(i, True, j, True)sat.add_clause(i, False, j, False)dict[k2] = -2if sat.satisfiable():print("YES")else:print("NO")