2-SAT
(Two_SAT.py)

View this file on GitHub
Last update: 2025-04-06 12:43:59+09:00

Outline

論理変数 $X_1, \dots, X_N$ 及び, これらの否定 $\lnot X_1, \dots, \lnot X_N$ をリテラルという.
リテラル $V_1, \dots, V_K$ の論理和 $V_1 \lor \dots \lor V_K$ を節という.

SATISFIABILITY (SAT) とは, 次のような問題である.

$2N$ 個のリテラルからなる論理式 $\varphi(X_1,\dots, X_N)$　に対して, これを $\mathbb{T}$ にするような $X_1, \dots, X_N$ への $\mathbb{T}, \mathbb{F}$ は存在するか?

また, SAT のうち, 次のような特別な場合には名前がついている.

CNF-SAT : $\varphi(X_1, \dots, X_N)$ が節の論理積からなっているもの.
2-SAT : CNF-SAT のうち, 全ての節の中のリテラルが高々2つであるもの.

つまり, 2-SAT とは次のような問題である.

リテラル全体の集合を $\mathcal{X}:=\{X_1, \ldots, X_N, \lnot X_1, \dots, \lnot X_N\}$ とする.

$j=1,2, \dots, M$ に対して, $F_j, G_j \in \mathcal{X}$ とする.
\[\varphi(X_1, \dots, X_N):=\bigwedge_{j=1}^M (F_j \lor G_j)\]
と定めるとき, $\varphi(X_1, \dots, X_N)=\mathbb{T}$ となるような　$X_1, \dots, X_N$ への $\mathbb{T}, \mathbb{F}$ の割り当ては存在するか?

Theory

$2N$ 頂点, $2M$ 辺の有向グラフ $D=(\mathcal{X}, A)$ を次のように定める.

$A:=\{\lnot F_j \Rightarrow G_j \mid 1 \leq j \leq M\} \cup \{\lnot G_j \Rightarrow F_j \mid 1 \leq j \leq M\}$

このとき, 以下は同値である.

充足可能
全ての $i=1,2, \dots, N$ に対して, $X_i$ と $\lnot X_i$ は異なる強連結成分に属している.

$D$ における強連結成分を $C_1 \sqsupset C_2 \sqsupset \dots \sqsupset C_P$ とし $X \in \mathcal{X}$ が属している連結成分が $C_p$ であるとき, $\gamma(X)=p$ と書くことにする.

このとき, $i=1,2, \dots, N$ に対して,

\[X_i=\begin{cases} \mathbb{T} & (\gamma(X_i)>\gamma(\lnot X_i)) \\ \mathbb{F} & (\gamma(X_i)<\gamma(\lnot X_i)) \end{cases}\]

が充足を可能にする一例になる.

※ $F \Rightarrow G$ への変換方法

変換前	変換後
$X \Rightarrow Y$	$X \Rightarrow Y$
$X \lor Y$	$\lnot X \Rightarrow Y$
$\lnot (X \land Y)$	$X \Rightarrow \lnot Y$
$X = Y$	$(X \Rightarrow Y) \land (\lnot X \Rightarrow \lnot Y)$
$X \neq Y$	$(X \Rightarrow \lnot Y) \land (\lnot X \Rightarrow Y)$
$X$	$\lnot X \Rightarrow X$
$\lnot X$	$X \Rightarrow \lnot X$

$Y_1=Y_2= \dots =Y_K$
- 以下の $K$ 個の含意の連言
  - $Y_1 \Rightarrow Y_2$
  - $Y_2 \Rightarrow Y_3$
  - $\vdots$
  - $Y_{K-1} \Rightarrow Y_K$
  - $Y_K \Rightarrow Y_1$
$Y_1, \dots, Y_K$ のうち, 高々1つが $\mathbb{T}$.
- $K$ 個の変数 $Z_1, \dots, Z_K$ を追加し, 以下の $(3K-2)$ 個の連言に帰着させる.
  - $Y_i \Rightarrow Z_i \quad (i=1,2, \dots, K)$
  - $Z_{i-1} \Rightarrow Z_i \quad (i=2,3, \dots, K)$
  - $\lnot (Y_i \land Z_{i-1}) \quad (i=2,3, \dots, K)$

Constructer

T=Two_SAT(N=0)

$N$ 変数の 2-SAT を定義する.
計算量 : $O(N)$ Time.

add_variable

T.add_variable(k=0)

$k$ 個の変数を新たに追加する.
計算量 : $O(k)$ Time.

add_impfy

T.add_imply(i, j)

節 $X_i \Rightarrow X_j$ を追加する.

add_or

T.add_or(i, j)

節 $X_i \lor X_j$ を追加する.

add_nand

T.add_nand(i, j)

節 $\lnot (X_i \land X_j)$ を追加する.

add_equivalent

T.add_equivalent(*I)

$I=(I_0, \dots, I_{n-1})$ に対して, 以下の $n$ 個の節を追加する.
- $X_{I_0} \Rightarrow X_{I_1}$
- $X_{I_1} \Rightarrow X_{I_2}$
- $\vdots$
- $X_{I_{n-2}} \Rightarrow X_{I_{n-1}}$
- $X_{I_{n-1}} \Rightarrow X_{I_0}$
これは $X_{I_0}=\dots=X_{I_n}$ であることと同値である.

add_not_equal

T.add_not_equal(i,j)

条件 $X_i \neq X_j$ を追加する.

add_true

T.add_true(i)

条件 $X_i$ を追加する.

add_false

T.add_false(i)

条件 $\lnot X_i$ を追加する.

at_most_one

T.at_most_one(*I)

次の条件を追加する.
- $X_i=\mathbb{T}$ となるような $i \in I$ は高々1つである (存在しなくても良い).

is_satisfy

T.is_satisfy(mode)

2-SAT が充足可能かどうかを判定する.
${\rm mode}$ の値と返り値
- ${\rm mode}=0$ : 充足可能ならば True, 充足不可能ならば False
- ${\rm mode}=1$ : 充足可能ならば, 充足例を $0,1$ で表したリスト, 充足不可能ならば None
- ${\rm mode}=2$ : $\gamma(X_i)=\gamma(\lnot X_i)$ となった $i$ 全てのリスト
計算量 : 変数の数を $N$, 節の数を $M$ としたとき, $O(N+M)$ Time.

solve

T.solve()

T.is_satisfy(1) と同等

Verified with

test_verify/yosupo_library_checker/Math/Two_Sat.test.py

Code

"""
変数 X_i の否定は ~i で宣言する.
例えば, ~0=-1 なので, X_{-1} は not X_0 を意味する.
"""

class Two_SAT:
    def __init__(self, N: int = 0):
        """ N 変数の 2-SAT を定義する.

        Args:
            N (int, optional): 変数の数. Defaults to 0.
        """

        self.N = N
        self.var_num = N

        self.arc: list[int] = [[] for _ in range(2 * N)]
        self.rev: list[int] = [[] for _ in range(2 * N)]

    def __var_to_index(self, v: int) -> int:
        """ 反転の情報を含んだ変数番号から, arc, rev におけるインデックスを求める.

        Args:
            v (int): 反転の情報を含んだ変数番号

        Returns:
            int: インデックス
        """

        return 2 * v if v >= 0 else 2 * (-v - 1) + 1

    def add_variable(self, k: int = 1) -> list[int]:
        """ 新たに k 個の変数を追加する

        Args:
            k (int, optional): 追加する変数の数. Defaults to 1.

        Returns:
            list[int]: 追加された変数の頂点番号のリスト
        """

        m = self.var_num
        self.var_num += k

        self.arc.extend([[] for _ in range(2*k)])
        self.rev.extend([[] for _ in range(2*k)])

        return list(range(m, m + k))

    def __add_clause(self,i,j):
        self.arc[self.__var_to_index(i)].append(self.__var_to_index(j))
        self.rev[self.__var_to_index(j)].append(self.__var_to_index(i))

    def add_imply(self, i: int, j: int):
        """ X_i -> X_j を追加する.

        Args:
            i (int): 変数番号
            j (int): 変数番号
        """

        self.__add_clause(i, j)
        self.__add_clause(~j, ~i)

    def add_or(self, i: int, j: int):
        """ X_i or X_j を追加する.

        Args:
            i (int): 変数番号
            j (int): 変数番号
        """

        self.add_imply(~i, j)

    def add_nand(self, i: int, j: int):
        """ not(X_i and X_j) を追加する

        Args:
            i (int): 変数番号
            j (int): 変数番号
        """

        self.add_imply(i, ~j)

    def add_equal(self, i: int, j: int):
        """ X_i = X_j を追加する.

        Args:
            i (int): 変数番号
            j (int): 変数番号
        """

        self.add_imply(i, j)
        self.add_imply(~i, ~j)

    def add_not_equal(self, i: int, j: int):
        """ X_i != X_j を追加する.

        Args:
            i (int): 変数番号
            j (int): 変数番号
        """

        self.add_equal(i, ~j)

    def add_equivalent(self, *I: int):
        """ I = [i_0, ..., i_{k-1}] に対して, X_{i_0} = ... = X_{i_{k-1}} を追加する.

        Args:
            I (int): 変数番号たち
        """

        if len(I) <= 1:
            return

        for j in range(len(I) - 1):
            self.add_imply(I[j], I[j + 1])

        self.add_imply(I[-1],I[0])

    def set_true(self, i: int):
        """ 変数 X_i を True にする.

        Args:
            i (int): 変数番号
        """

        self.__add_clause(~i, i)

    def set_false(self, i: int):
        """ 変数 X_i を False にする.

        Args:
            i (int): 変数番号
        """

        self.__add_clause(i, ~i)

    def at_most_one(self, *I: int):
        """X_i (i in I) を満たすような i は高々1つだけという条件を追加する.

        Args:
            I (int): 変数番号の配列
        """

        # k = 1 のときの条件は無意味
        if (k := len(I)) <= 1:
            return

        A = self.add_variable(k)

        self.add_imply(I[0], A[0])
        for i in range(1, k):
            self.add_imply(A[i - 1], A[i])
            self.add_imply(I[i], A[i])
            self.add_nand(A[i - 1],I[i])

    def calculate(self):
        n = self.var_num
        group = [0] * (2 * n)
        order = []

        for s in range(2 * n):
            if group[s]:
                continue

            stack = [s]
            group[s] = -1

            while stack:
                u = stack.pop()
                for v in self.arc[u]:
                    if group[v]:
                        continue

                    group[v] = -1

                    stack.append(u)
                    stack.append(v)
                    break
                else:
                    order.append(u)

        k = 0
        for s in reversed(order):
            if group[s] != -1:
                continue

            stack = [s]
            group[s] = k

            while stack:
                u = stack.pop()
                for v in self.rev[u]:
                    if group[v] != -1:
                        continue

                    group[v] = k
                    stack.append(v)
            k += 1

        ans = [None] * n
        for i in range(n):
            if group[2 * i] > group[2 * i + 1]:
                ans[i] = True
            elif group[2 * i] < group[2 * i + 1]:
                ans[i] = False
            else:
                self.__satisfiability = False
                self.__ans = None
                self.__self_contradiction = []
                return
        else:
            self.__satisfiability = True
            self.__ans = ans
            self.__self_contradiction = [i for i in range(self.var_num) if group[2 * i] == group[2 * i + 1]]

    @property
    def is_satisfiable(self):
        return self.__satisfiability

    @property
    def ans(self):
        return self.__ans

    @property
    def self_contradiction(self):
        return self.__self_contradiction

Traceback (most recent call last):
  File "/opt/hostedtoolcache/Python/3.13.3/x64/lib/python3.13/site-packages/onlinejudge_verify/documentation/build.py", line 71, in _render_source_code_stat
    bundled_code = language.bundle(stat.path, basedir=basedir, options={'include_paths': [basedir]}).decode()
                   ~~~~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/opt/hostedtoolcache/Python/3.13.3/x64/lib/python3.13/site-packages/onlinejudge_verify/languages/python.py", line 96, in bundle
    raise NotImplementedError
NotImplementedError

library_for_python

2-SAT
(Two_SAT.py)

Outline

Theory

Contents

Constructer

add_variable

add_impfy

add_or

add_nand

add_equivalent

add_not_equal

add_true

add_false

at_most_one

is_satisfy

solve

Verified with

Code

2-SAT (Two_SAT.py)

Outline

Theory

Contents

Constructer

add_variable

add_impfy

add_or

add_nand

add_equivalent

add_not_equal

add_true

add_false

at_most_one

is_satisfy

solve

Verified with

Code

2-SAT
(Two_SAT.py)