YukiCoder 274 The Wall と 2-SATの復元

https://yukicoder.me/problems/no/274

2-SATの復元の情報が少ないので記録。

# 2-SATについて
詳しい説明は蟻本やGoogleに譲る。例をあげると、

>２値(例えばTrue/False)で表現できる変数があり、それらの真偽条件の制約があったとする。例えば、$a, b, c$の3つの変数があった際に、
$ a \rightarrow \lnot b$
が与えられる。この時、
$ \lnot a \rightarrow  b$
は自明である。この条件を満たすのは「$a , \lnot b$」か「$\lnot a , \lnot b$」で、$c$は$c$でも$\lnot c$でも良い.

この場合は解があるが、そもそも、この問題が「解けるかどうか」を判別するのが2-充足可能性問題である。これは以下のように解く。

- $a,b,c,\lnot a,\lnot b,\lnot c$の6つのノードがある有向グラフを作る
- 各条件を、互いのノードに対する辺(有向)で表現する(互いになので２本張る)
- グラフを強連結成分分解する
- 全ての変数において(例えば今$x$を考えると)$x$と$\lnot x$が同一の強連結成分に属さない場合、充足可能である。そうでない場合、充足不可能である。

# The Wallを2-SATで解く
問題は原文に譲る。例えば、下のようなブロックが4段あったとする。(例の「良いブロック」)
<img src="https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/30938/9dfe9b26-de4b-d2ea-eb42-17d316c05bab.png" width=50%>

この各段は180度ひっくり返すことができる(つまり、以下の赤いブロックにできる)
<img src="https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/30938/d07c0d39-f10e-cfde-883d-d09c069ffc73.png" width=50%>

この場合、図を見ればわかるが、$aとb$はなんでもよく(ひっくり返してもそのままでも他のブロックと干渉しないから)$c$と$d$は両方そのままか、両方ひっくり返さないといけないことが分かる。

つまり、以下のように考える。

- 下から1段ずつ見ていき、今の行をx行目とする。
- x行目よりも上の列をしたから1段ずつ見ていき、その行をy行目とする
- xがそのままでyと衝突しない場合、yをひっくり返してみても衝突しないなら、何もしない（その2つは干渉しないので）
- xがそのままでyと衝突しない場合、yをひっくり返してみると衝突するなら、$x \rightarrow y$であり$ \lnot x \rightarrow \lnot y $である。つまり、片方だけひっくり返すと干渉する。
- xがそのままでyと衝突する場合、yをひっくり返してみて通るなら、$x \rightarrow \lnot y$であり$ \lnot x \rightarrow y $である。つまり、片方だけひっくり返さなければならない。
- xがそのままでyと衝突する場合、yをひっくり返しても衝突するなら、何をしても通らない。

これらを、(上記の図で考えるなら)$a,b,c,d,\lnot a,\lnot b,\lnot c,\lnot d$のノードに対して処理(条件があるならば有向の辺を張る)し、強連結成分分解し判定を行う。

# 2-SATで解いた後の復元

YukiCoderのサンプル4の場合、次のような図であり、
<img src="https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/30938/b66fcae5-0ea9-6a2e-b326-49e1a07d140c.png" width=50%>

強連結分解の結果、$[5, 4, 3, 2, 1, 1, 0, 2, 3, 5]$となる。これらはそれぞれ、[$a,b,c,d,e,\lnot a,\lnot b,\lnot c,\lnot d, \lnot e$]を示す。
これを図にすると、以下のようになる。
<img src="https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/30938/ee6820fe-aa8e-4066-0c7b-7e70780dfbe1.png" width=50%>

さて、ここで、冒頭で、

> $ a \rightarrow \lnot b$
が与えられる。この時、
$ \lnot a \rightarrow  b$

であったことを思い出す。このため、各強連結成分$x$内のノードすべてにおいて、その対となる(notの)ノードはすべて$y(\neq x)$である。例えば、上の図では、$a, \lnot e$は強連結成分5に属するが、その対となる(notの)ノード$ \lnot a, e $は同じ強連結成分1に属する。

違う例を挙げる。
<img src="https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/30938/ec9adc3f-4256-52b3-e2af-22b450525c40.png" width=50%>
このような強連結成分分解の結果となった場合、黒い強連結成分1の対となるノードはすべて黄色の強連結成分2になっていることが分かる。

# 結論
このため、n個のノードに対して(つまり、上のノードだけに関して)対となるノードよりも大きければTrue, 小さければFalseを返すことで復元ができる。(ここで、対となるノードの強連結成分は充足可能である時点で必ず異なることが分かっている。)

# コード
```Python
import sys

sys.setrecursionlimit(200000)

from collections import deque
# a-zに正方向と逆辺を張る
def addEdge(g, a, z):
    g[0][a].append(z)
    g[1][z].append(a)
    g[0][z].append(a)
    g[1][a].append(z)

# グラフの初期化
def initGraph(g, edgenum):
    g.append([])  # [0] 正方向のグラフ
    g.append([])  # [1] 逆方向のグラフ
    for _ in range(edgenum):
        g[0].append(deque(list()))
    for _ in range(edgenum):
        g[1].append(deque(list()))

def dfs(g, v, visited, vs):
    # 正方向のDFS
    visited[v] = True
    for i in range(len(g[0][v])):
        if visited[g[0][v][i]] is False:
            dfs(g, g[0][v][i], visited, vs)
    vs.append(v)

def rdfs(g, v, visited, cmp, k):
    # 逆方向のDFS
    # kがcall元に指定される連結成分の通し番号
    visited[v] = True
    cmp[v] = k
    # 指定したノードの逆辺をたどる
    for i in range(len(g[1][v])):
        # print("go? {0}".format(g[1][v][i]))
        # 逆辺の先がrDFSで到達できないときのみ
        if visited[g[1][v][i]] is False:
            # print("yes")
            rdfs(g, g[1][v][i], visited, cmp, k)

def scc(g, cmp):
    vs = []  # 帰りがけのリスト
    visited = [False] * len(g[0])
    cmp.extend([None] * len(g[0]))
    for i in range(len(g[0])):
        if visited[i] is False:
            dfs(g, i, visited, vs)

    visited = [False] * len(g[1])
    k = 0
    # pprint(vs)
    for i in range(len(vs) - 1, -1, -1):
        # print("vited: i={0} vs[i] = {1}".format(i, vs[i]))
        # print(visited)
        if visited[vs[i]] is False:
            # print("rdfs [{0}]".format(i))
            rdfs(g, vs[i], visited, cmp, k)
            k += 1
    # pprint(vs)
    return k # 何個の強連結成分に分かれたか？


n, m = map(int, input().split())
dat = []
for _ in range(n):
    a,b = map(int, input().split())
    dat.append((a,b))

f = True

vCount = n * 2  # 各xとnot x分で2倍
# 0-n-1が各要素のx, n - n*2-1がnot x の 領域

g = []  # グラフ。[0] = 正方向のグラフ。 [1] = 逆方向のグラフ
cmp = [] # 強連結成分を記録する

from pprint import pprint
initGraph(g, edgenum=vCount)

def isSafe(a, b, c, d):
    a,b,c,d = min(a,b), max(a,b), min(c,d), max(c,d)
    #print("{0} {1} {2} {3}".format(a,b,c,d))
    if a < c and b < c:
        #print("T")
        return True
    if a > d and b > d:
        #print("T2")
        return True
    #print("{0} {1} {2} {3}".format(a,b,c,d))
    #print("F")
    return False

for i in range(n):
    if f is False:
        break
    # 自分より上のブロックに対する制約をすべて確認する
    for j in range(i+1, n):

        if isSafe(dat[i][0], dat[i][1], dat[j][0], dat[j][1]) is False:
            # もし、そのままで衝突する場合、
            if isSafe((m-1) - dat[i][0], (m-1) - dat[i][1], dat[j][0], dat[j][1]):
                # 自分を反転して通るのであれば not x → y, あるいはx → not yを満たさないとならないので制約を張る
                addEdge(g, n + i, j)
                addEdge(g, i, n + j)
            else:
                # 何をしても通らない制約を張る x → not xを張る(絶対にこれは満たせない)
                addEdge(g, i, n+i)
                # 続けてもいいがどうせ満たせないので抜ける
                break

        else: # そのままで通る場合で
            if isSafe((m-1) - dat[i][0], (m-1) - dat[i][1], dat[j][0], dat[j][1]) is False:
                # 反転させてしまうと通らないのであれば、 x → y あるいは not x → not yなのだから
                addEdge(g, i, j)
                addEdge(g, n + i, n + j)
            else:
                # 回転させても通るならなにをしても通るので制約は要らない
                pass

k = scc(g, cmp)
l = []
f = True
# ここが復元のコード
for i in range(n):
    if cmp[i] == cmp[n+i]:
        f = False
        break
    if cmp[i] > cmp[n+i]:
        l.append(True)
    else:
        l.append(False)
# 判定結果
print("YES" if f else "NO")
# 強連結成分の列挙
print(cmp)
# 結果の復元の列挙
print(l)
```