第7章 SATで数独を解く

左上のマスに1が入るか、2が入るか、という候補を真偽値で表します。「左上は1」を 表す変数が真なら、そのマスに1を置きます。同様に81個のマスと9個の数字を組み合わせると、 \(81\times9=729\) 個の真偽変数ができます。

この729個へ、同じマスの候補を一つだけ真にする条件や、同じ行で同じ数字を重ねない条件を 加えます。すべての条件を満たす真偽値の組が、完成盤面に対応します。このように命題論理式を 満たす真偽値の割り当てを探す問題が SAT（充足可能性問題） です。

この章では、Pythonから PySAT を使い、SAT専用ソルバーの MiniSat 2.2へ論理式を渡します。Pythonは論理式への変換と盤面の復元を担当します。実際の探索は MiniSatのCDCLアルゴリズムが行います [1] [2]。

二つの候補から一つを選ぶ

真か偽のどちらかを取る記号を 命題変数 と呼びます。変数 \(x_1\) と \(x_2\) の ちょうど一方を真にする条件は、次の式で書けます。

\(\lor\) はOR（少なくとも一方）、\(\land\) はAND（両方）、\(\lnot\) はNOT （真偽の反転）を表します。

\[(x_1 \lor x_2) \land (\lnot x_1 \lor \lnot x_2)\]

前半は「少なくとも一つは真」、後半は「二つを同時に真にはしない」という条件です。 \(x_1\) や \(\lnot x_1\) を リテラル、リテラルをORでつないだ \((x_1\lor x_2)\) を 節 と呼びます。節をANDでつないだ式は 連言標準形、略して CNFです。

二つの候補に対する式の真偽

\(x_1\)	\(x_2\)	\(x_1\lor x_2\)	\(\lnot x_1\lor\lnot x_2\)	式全体
偽	偽	偽	真	偽
偽	真	真	真	真
真	偽	真	真	真
真	真	真	偽	偽

PySATでは、変数を1以上の整数で表します。正の 1 は \(x_1\)、負の -1 は \(\lnot x_1\) です。一つの節は整数のリスト、CNF全体は節のリストになります。 式全体を真にする真偽値の割り当てを モデル と呼びます。

def exactly_one_of_two() -> tuple[tuple[bool, bool], ...]:
    # 1個以上を真にする節と、2個同時には真にしない節です。
    clauses = [[1, 2], [-1, -2]]
    answers: list[tuple[bool, bool]] = []

    with Minisat22(bootstrap_with=clauses) as solver:
        while solver.solve():
            model = solver.get_model()
            positive = {literal for literal in model if literal > 0}
            answer = (1 in positive, 2 in positive)
            answers.append(answer)

            # 今得た真偽値の組を禁止し、次のモデルを探します。
            blocking_clause = [
                -variable if value else variable
                for variable, value in enumerate(answer, start=1)
            ]
            solver.add_clause(blocking_clause)

    return tuple(sorted(answers))

最初のモデルを得た後、その真偽値の組だけを禁止する節を追加します。この ブロッキング節 により、同じ論理式から次のモデルを探索します。結果は二通りです。

formula: (x1 OR x2) AND (NOT x1 OR NOT x2)
model 1: x1=false x2=true
model 2: x1=true x2=false

たとえば最初のモデルが \(x_1=\mathrm{false}, x_2=\mathrm{true}\) なら、追加する節は \(x_1\lor\lnot x_2\)、PySATのリストでは [1, -2] です。この節はその真偽値の組でだけ 偽になるため、同じモデルを除いてもう一方を残します。

数独でも、完成盤面に対応するモデルを禁止してもう一度解くことで、二つ目の解を調べます。

「ちょうど一つ」をCNFにする

\(n\) 個の変数 \(x_1,\ldots,x_n\) のちょうど一つを真にするには、少なくとも一つを真にする 節を1個置きます。

\[x_1 \lor x_2 \lor \cdots \lor x_n\]

さらに、異なる二つの変数を同時に真にしない節を、すべての組に置きます。

\[\bigwedge_{1\le i<j\le n}(\lnot x_i \lor \lnot x_j)\]

後半には \(\binom{n}{2}\) 個の節があります。数独では \(n=9\) なので、9個の候補に対する exactly-one制約は、長さ9の節1個と、長さ2の節36個です。

def exactly_one(literals: list[int]) -> list[list[int]]:
    clauses = [literals]
    # どの2個も同時に真にならないよう、すべての組に禁止節を加えます。
    clauses.extend([-left, -right] for left, right in combinations(literals, 2))
    return clauses

たとえば exactly_one([1, 2, 3]) は、少なくとも一つを選ぶ [1, 2, 3] と、二つを同時に 選ばない [-1, -2]、[-1, -3]、[-2, -3] を返します。

この方式は、すべての組を直接並べるため pairwise encoding と呼ばれます。補助変数を使って 節数を減らす符号化もありますが、ここでは生成された節と数独の規則を対応させやすい方式を 選びました。PySAT自体も複数の基数制約符号化を提供しています [3]。

候補を729個の変数へ写す

行 \(r\)、列 \(c\) のマスに数字 \(d\) が入ることを、命題変数 \(X_{r,c,d}\) で表します。行と列は0から8、数字は1から9とします。Pythonのリストへ渡せる 整数IDは次の式で計算します。

\[v(r,c,d)=81r+9c+d\]

\(v(0,0,1)=1\) で、最後の候補 \(v(8,8,9)=729\) です。 たとえば \(v(0,0,5)=5\) の 5 は数独へ入れる数値そのものではなく、「左上のマスが5」 という命題変数をMiniSatへ渡すための識別番号です。

def candidate_var(row: int, col: int, digit: int) -> int:
    """Return the SAT variable for ``cell[row, col] == digit``."""
    return row * 81 + col * 9 + digit

数独のSAT符号化を研究したLynceとOuaknineも、この候補表現を使っています [4]。数字の大小や足し算は扱いません。729個は互いに独立した真偽変数であり、 整数IDは変数を区別する識別子として用います。この点で、第8章「SMT」で扱う整数や配列の理論とは 入力の意味が異なります。

四種類のexactly-one制約

数独の規則を、次の四種類のグループへ分けます。

各マス

\(X_{r,c,1},\ldots,X_{r,c,9}\) のちょうど一つを真にします。グループは81個です。

行と数字

行 \(r\) のどの列に数字 \(d\) を置くかを一つにします。行9本と数字9個で81個です。

列と数字

列 \(c\) のどの行に数字 \(d\) を置くかを一つにします。これも81個です。

ブロックと数字

各3×3ブロックで、数字 \(d\) を置く場所を一つにします。9ブロックと9数字で81個です。

合計324個のグループがあり、一つにつき37節を生成します。初期配置を除くCNFは \(324\times37=11{,}988\) 節です。初期配置は、対応する \(X_{r,c,d}\) を真にする長さ1の 節、つまり 単位節 として追加します。

def sudoku_cnf(givens: Board) -> list[list[int]]:
    side, box_side = board_geometry(givens)
    if side != 9:
        raise ValueError("this example supports 9x9 Sudoku only")

    clauses: list[list[int]] = []

    # 各マスには、1〜9のうちちょうど一つが入ります。
    for row in range(side):
        for col in range(side):
            clauses.extend(
                exactly_one([candidate_var(row, col, digit) for digit in range(1, side + 1)])
            )

    # 各行では、それぞれの数字がちょうど一度だけ現れます。
    for row in range(side):
        for digit in range(1, side + 1):
            clauses.extend(
                exactly_one([candidate_var(row, col, digit) for col in range(side)])
            )

    # 各列にも、同じexactly-one制約を置きます。
    for col in range(side):
        for digit in range(1, side + 1):
            clauses.extend(
                exactly_one([candidate_var(row, col, digit) for row in range(side)])
            )

    # 各3×3ブロックでも、それぞれの数字を一つに絞ります。
    for box_row in range(0, side, box_side):
        for box_col in range(0, side, box_side):
            for digit in range(1, side + 1):
                block = [
                    candidate_var(row, col, digit)
                    for row in range(box_row, box_row + box_side)
                    for col in range(box_col, box_col + box_side)
                ]
                clauses.extend(exactly_one(block))

    # 初期配置は、対応する候補変数を真にする単位節です。
    for position, given in enumerate(givens):
        if given:
            row, col = divmod(position, side)
            clauses.append([candidate_var(row, col, given)])

    return clauses

四種類すべてへ「少なくとも一つ」と「高々一つ」を入れるため、同論文の分類では 拡張符号化（extended encoding）に当たります。数独の解を変えない重複した条件も含みますが、単位伝播で値が 決まりやすくなる利点があります [4]。

clauses は、そのまま DIMACS CNF に書き出せる形です。DIMACSでは p cnf 729 12013 のようなヘッダーを書き、各節の末尾へ 0 を付けます。PySATのPython APIは 変数数を節から読み取るため、コード中ではヘッダーと末尾の 0 を省いています。

MiniSatはCNFをどう調べるか

人間とソルバーの役割分担

段階	人間（Pythonコード）が行うこと	ソルバー（MiniSat）が行うこと
入力	729個の命題変数を定義し、数独の規則をCNF（節のリスト）へ変換する	―
探索	―	CNFを受け取り、CDCL（単位伝播・決定・競合解析と節学習）で充足する割り当てを探す
出力	正のリテラルを候補に戻し、盤面を復元・検証する	モデル（正負の整数のリスト）または UNSAT を返す

ここからは、ソルバー内部で行われる発展的な処理の概要です。MiniSat 2.2は CDCL （Conflict-Driven Clause Learning）方式のSATソルバーです。探索中には、 おおむね次の処理が起こります。

単位伝播

節に未確定のリテラルが一つしか残らなければ、そのリテラルを真にします。たとえば初期配置で \(X_{0,0,5}\) が真になると、同じマスのpairwise節からほかの8候補が偽になります。

決定

伝播だけで値が決まらなければ、未確定の変数を選んで真偽値を仮定します。どの変数を選ぶかは ソルバーのヒューリスティックが決めます。

競合解析と節学習

ある節のリテラルがすべて偽になると競合です。CDCLは競合へ至った代入を解析し、同種の競合を 避ける節を学習します。その節を使い、必要な位置まで代入を戻します。

MiniSatは、バックトラックへ単位伝播、節学習、非時系列の巻き戻しを組み合わせます。学習節は 元のCNFから論理的に導けるため、解を失わずに探索範囲を狭められます。CDCLの健全性と完全性は SATの標準的な解説でも扱われています [5]。実装からは PySATのソルバーAPI を通して MiniSatを呼び出します。

モデルを盤面へ戻す

MiniSat22.get_model() は、正負の整数を並べたモデルを返します。正の整数に対応する候補だけを 集め、各マスで真になった数字を一つずつ取り出します。

def decode_model(model: list[int]) -> Board:
    positive = {literal for literal in model if literal > 0}
    cells: list[int] = []
    for row in range(9):
        for col in range(9):
            digits = [
                digit
                for digit in range(1, 10)
                if candidate_var(row, col, digit) in positive
            ]
            if len(digits) != 1:
                raise ValueError(f"model does not choose one digit at row {row}, col {col}")
            cells.append(digits[0])
    return tuple(cells)

各マスにexactly-one制約があるため、正しいモデルなら digits の長さは必ず1です。コードでも この条件を確認し、CNF生成や復元処理の誤りを見逃さないようにしています。復元後の盤面は、さらに 共通検証器で行、列、ブロックと初期配置を検査します。

別解を探す

一つのモデルを得た後、完成盤面で真だった81個の候補をすべて反転した節を追加します。たとえば 完成盤面の真の候補が \(p_1,\ldots,p_{81}\) なら、ブロッキング節は次のとおりです。

\[\lnot p_1 \lor \lnot p_2 \lor \cdots \lor \lnot p_{81}\]

この節は、81個の候補がすべて再び真になる場合だけ偽です。ほかの完成盤面は残ります。

def solve(givens: Board, limit: int = 2) -> Result:
    if limit < 1:
        raise ValueError("limit must be positive")

    clauses = sudoku_cnf(givens)
    clue_clauses = sum(value != 0 for value in givens)
    found: list[Board] = []
    solve_calls = 0

    with Minisat22(bootstrap_with=clauses) as solver:
        # 表示数より一つ多く探し、まだ別解があるかも確認します。
        while len(found) <= limit:
            solve_calls += 1
            if not solver.solve():
                exhausted = True
                break

            model = solver.get_model()
            if model is None:
                raise RuntimeError("MiniSat returned SAT without a model")
            board = decode_model(model)
            found.append(board)

            # 完成盤面を禁止して、同じCNFから次の解を探します。
            solver.add_clause(block_board(board))
        else:
            exhausted = False

    solutions = tuple(found[:limit])
    status = "solved" if solutions else "unsat"
    return Result(
        status=status,
        solutions=solutions,
        exhausted=exhausted,
        variables=VARIABLES,
        base_clauses=BASE_CLAUSES,
        clue_clauses=clue_clauses,
        solve_calls=solve_calls,
    )

表示要求数より1個多くモデルの生成を試みます。後続の solve() が False を返す状態は、 追加されたブロッキング節によって解空間上の全解が走査され、解の列挙が完了したことを示します。

実行する

サンプルプログラムは examples/06-sat/ にあります。詳しい実行手順やオプションについては examples/06-sat/README.md を参照してください。

通常問題

通常問題には25個の初期配置があるため、CNF全体で12,013節となります。最初に満たすモデルを得た後、その盤面を禁止するブロッキング節を追加して再度探索すると非充足となるため、一意解であることが判定できます。

解がない問題

矛盾問題では、12,018節を同時に満たす割り当てが存在しません。初回の判定で非充足となるため、解なし（unsat）と確定します。

解が複数ある問題

複数解問題では、最初のモデルを禁止した後も2つ目のモデルが得られます。2つ目のモデルを禁止した段階で非充足となることから、解が全部で2つ存在することが判定されます。

この方法で分かること

CNFの各モデルからは数独の完成盤面が一つ得られ、すべての完成盤面はCNFのモデルになります。 この対応があるため、MiniSatが SAT と返せば解が存在し、UNSAT と返せば解は存在しません。 ブロッキング節を追加して二回目が UNSAT になれば一意解です。サンプルコードは乱数を 指定していません。モデルが見つかる順序はソルバーの版やヒューリスティックで変わる場合が ありますが、SATかUNSATかという判定と解集合は変わりません。

pairwise encodingは、補助変数を使わずにexactly-one制約を読める点が長所です。その代わり、候補数 \(n\) に対して節数が \(O(n^2)\) になります。大きな数独や別の組合せ問題では、逐次カウンタ など別の符号化が適する場合があります。どの符号化を選んでも、SATソルバーへ渡す前に問題を 真偽変数とCNFへ変換し、返されたモデルを元の問題へ戻す流れは共通です。

参考文献

[1]

Niklas Eén and Niklas Sörensson. An Extensible SAT-solver. In Theory and Applications of Satisfiability Testing – SAT 2003, volume 2919 of Lecture Notes in Computer Science, 502–518. 2003. doi:10.1007/978-3-540-24605-3_37.

[2]

Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva. PySAT: A Python Toolkit for Prototyping with SAT Oracles. In Theory and Applications of Satisfiability Testing – SAT 2018, volume 10929 of Lecture Notes in Computer Science, 428–437. 2018. doi:10.1007/978-3-319-94144-8_26.

[3]

PySAT Developers. PySAT Documentation. 2026. URL: https://pysathq.github.io/docs/html/ (visited on 2026-08-08).

[4] (1,2)

Inês Lynce and Joël Ouaknine. Sudoku as a SAT Problem. In Proceedings of the 9th International Symposium on Artificial Intelligence and Mathematics. 2006. URL: https://people.mpi-sws.org/~joel/publications/sudoku05.pdf.

[5]

Joao Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-Driven Clause Learning SAT Solvers. In Handbook of Satisfiability, pages 131–153. IOS Press, 2009. URL: https://www.cs.princeton.edu/~zkincaid/courses/fall18/readings/SATHandbook-CDCL.pdf.