第12章 Boolean Gröbner基底で数独を解く¶

二つの候補 \(x,y\) から一つだけ選ぶ場面を、連立方程式にしてみます。選ぶ候補を1、選ばない候補を0とすれば、次の三本で表せます。

\[x^2-x=0,\qquad y^2-y=0,\qquad x+y-1=0\]

最初の二本は、それぞれの変数を0か1に限ります。たとえば \(x^2-x=x(x-1)\) なので、この式が0になるのは \(x=0\) または \(x=1\) のときだけです。最後の一本は、二変数のうち一つを1にします。この連立方程式を解けば、\((x,y)=(1,0)\) と \((0,1)\) が得られます。

変数が増えると、元の方程式を眺めるだけでは解を取り出しにくくなります。そこで、同じ共通解を持ち、変数を順に消去しやすい方程式の組へ変換します。この組が Gröbner基底です。線形連立方程式を行基本変形で階段状にする操作を、多項式へ広げたものに相当します。

方程式を解きやすい形へ変える¶

小さな例を SymPy 1.14.0 で計算します。

"""Compute a lexicographic Gröbner basis for an exactly-one condition."""

from sympy import QQ, groebner, solve_poly_system, symbols


def main() -> None:
    x, y = symbols("x y")
    equations = (
        x**2 - x,
        y**2 - y,
        x + y - 1,
    )

    # 辞書式順序ではxをyより先に置き、yだけの式が基底に現れるようにする。
    basis = groebner(equations, x, y, order="lex", domain=QQ)

    print("input equations:")
    for equation in equations:
        print(f"  {equation} = 0")
    print("groebner basis (lex, x > y):")
    for polynomial in basis.polys:
        print(f"  {polynomial.as_expr()} = 0")

    # 基底は元の連立方程式と同じ解を持つので、基底から二解を復元できる。
    solutions = solve_poly_system(
        [polynomial.as_expr() for polynomial in basis.polys],
        x,
        y,
        strict=True,
    )
    print("solutions:")
    for solution in solutions:
        print(f"  x={solution[0]}, y={solution[1]}")


if __name__ == "__main__":
    main()

input equations:
  x**2 - x = 0
  y**2 - y = 0
  x + y - 1 = 0
groebner basis (lex, x > y):
  x + y - 1 = 0
  y**2 - y = 0
solutions:
  x=0, y=1
  x=1, y=0

入力した三本は、二本のGröbner基底へ変わりました。

\[x+y-1=0,\qquad y^2-y=0\]

後ろの式は \(y\) だけを含むので、まず \(y=0,1\) を求められます。その値を前の式へ代入すれば、\(x=1-y\) です。元の三本と基底の二本は見た目が違いますが、共通解は変わりません。

Gröbner基底を計算するときは、\(x^2\) や \(xy\) のような各項をどの順に比較するかを決めます。これが 単項式順序 です。この例では、\(x\) を \(y\) より先に比較する辞書式順序 lex を使いました。 x > y とすると、優先順位の高い \(x\) を含む項から消去しやすい形に整理されます。この例では \(y\) だけの方程式が基底に残るため、最後の変数から逆向きに解けます。変数順や単項式順序が変われば基底の形や計算量も変わりますが、表す共通解は同じです。 SymPyの groebner は lex、grlex、grevlex を選べます [1]。

補足

入力した多項式から加算と多項式倍で作れる式全体を イデアル と呼びます。Gröbner基底は、そのイデアルを生成し直した多項式の組です。本手法は共通解を保ったまま、変数を順に消去しやすい形式へ変換する操作に相当します。

人間とソルバーの役割分担¶
段階	人間（Pythonコード）が行うこと	計算エンジン（SymPy）が行うこと
入力	候補をBoolean変数にし、各組の和が1になる多項式と \(x^2 - x = 0\) を立てる	―
変換	―	辞書式順序のGröbner基底を計算し、同じ共通解を持つ変数消去しやすい多項式の組へ変換する
出力	基底から得た各変数の値を盤面へ復元・検証する	基底の多項式、または定数 \(1\)（共通解なし）を返す

候補をBoolean変数にする¶

4×4数独を使います。行 \(r\)、列 \(c\) のマスへ数字 \(d\) を置く候補を \(x_{r,c,d}\) とし、置くなら1、置かないなら0にします。各候補へ次の方程式を加えます。

\[x_{r,c,d}^2-x_{r,c,d}=0\]

この章の「Boolean」は、候補変数が0か1を取ることを指します。計算する係数体は有理数体 \(\mathbb{Q}\) です。有理数体では、候補 \(v_1,\ldots,v_k\) から一つだけ選ぶ条件を次の一次方程式で書けます。

\[v_1+\cdots+v_k-1=0\]

この式を、次の四種類について作ります。

一つのマスに入る数字
一つの行に置く各数字
一つの列に置く各数字
一つの2×2ブロックに置く各数字

たとえばマス \((1,2)\) に残った候補が2と4なら、 \(x_{1,2,2}+x_{1,2,4}-1=0\) を加えます。2を置く解では前者が1、後者が0になり、 4を置く解ではその反対になります。

Boolean変数の和が1なので、どの組でも一候補だけが選ばれます。Arnoldらは、4×4数独を64個の Boolean変数と多項式で表す方法を示しています [2]。

補足: GF(2)のBoolean多項式環との違い

PolyBoRiのような専用処理系は、係数を0と1だけ持つ体 \(\mathrm{GF}(2)\) 上のBoolean 多項式環を扱います [3]。GF(2)では \(1+1=0\) です。候補が三つ以上あるとき、和を1にする式だけでは「一つ」に限らず、三つ同時に選ぶ場合も通ります。「高々一つ」の方程式を加えるなど、GF(2)に合う符号化が必要です。

今回の環境にはSageMath、PolyBoRi、Singular、Macaulay2がありませんでした。処理系だけを SymPyへ置き換え、PolyBoRi向けの式をそのまま使ったわけではありません。有理数体を選んだため、 候補の和 - 1 = 0 がちょうど一つを表します。

初期配置から直接消せる候補を除く¶

空の4×4盤面なら、候補変数は \(4\times4\times4=64\) 個です。サンプルでは、初期配置と同じ行、列、ブロックにある同じ数字の候補を、方程式を作る前に除きます。たとえば左上に1があれば、同じ行、列、ブロックの 1 候補は変数にしません。初期配置の数字そのものも固定済みなので変数にしません。

この候補除去は、Gröbner基底が導いた結果ではありません。数独の初期配置だけを使った前処理です。候補が一つになったマスを繰り返し確定する処理まではしません。前処理後の候補を変数にし、 Boolean方程式と各組の和の方程式を作ります。

def build_polynomial_model(givens: Board) -> PolynomialModel:
    if len(givens) != SIZE * SIZE:
        raise ValueError("この例は4×4数独だけを扱います")

    sudoku_units = units(givens)
    polynomials: list[Expr] = []

    # 初期配置だけで同じ数字が重複していれば、1 = 0を加えて矛盾を表す。
    for unit in sudoku_units:
        fixed = [givens[position] for position in unit if givens[position]]
        if len(fixed) != len(set(fixed)):
            polynomials.append(Integer(1))

    candidate_digits: dict[int, tuple[int, ...]] = {}
    for position, given in enumerate(givens):
        if given:
            continue
        related = {
            other
            for unit in sudoku_units
            if position in unit
            for other in unit
        }
        candidate_digits[position] = tuple(
            digit
            for digit in range(1, SIZE + 1)
            if all(givens[other] != digit for other in related)
        )

    candidate_keys = tuple(
        (position, digit)
        for position in sorted(candidate_digits)
        for digit in candidate_digits[position]
    )
    variables = tuple(Symbol(variable_name(*key)) for key in candidate_keys)
    candidate_variables = dict(zip(candidate_keys, variables, strict=True))

    # x(x - 1) = 0を加え、各候補変数を0または1に限る。
    polynomials.extend(variable * (variable - 1) for variable in variables)

    # 各空きマスでは、残った候補変数の和を1にする。
    for position, digits in candidate_digits.items():
        choices = [candidate_variables[position, digit] for digit in digits]
        polynomials.append(sum(choices, Integer(0)) - 1)

    # 行、列、ブロックごとに、まだ置かれていない数字を一度だけ選ぶ。
    for unit in sudoku_units:
        for digit in range(1, SIZE + 1):
            fixed_count = sum(givens[position] == digit for position in unit)
            if fixed_count > 1:
                polynomials.append(Integer(1))
            elif fixed_count == 0:
                choices = [
                    candidate_variables[position, digit]
                    for position in unit
                    if (position, digit) in candidate_variables
                ]
                polynomials.append(sum(choices, Integer(0)) - 1)

    return PolynomialModel(
        givens=givens,
        variables=variables,
        candidate_variables=candidate_variables,
        polynomials=tuple(polynomials),
    )

通常問題では64候補が24変数、複数解問題では8変数、矛盾問題では28変数まで減りました。これは初期配置が異なるためです。出力の variables は前処理後、input_polynomials は基底計算へ実際に渡した方程式の本数を表します。

強い初期配置の4×4に限る理由¶

9×9数独を同じ候補表現へ素直に広げると、変数は \(9\times9\times9=729\) 個になります。Gröbner基底の計算では、途中の多項式が入力より大きくなることがあり、変数順にも強く影響されます。Arnoldらの論文でも4×4を説明用に採用し、初期配置のない9×9を同種の方法で扱う計算は一般的なデスクトップの範囲を超えると報告しています [2]。

本章は、一般用途のSymPyで基底計算まで再現できることを優先しました。4×4でも、初期配置から直接除ける候補が多い三問だけを使います。この結果から、空の4×4や9×9も同じ時間で解けるとは言えません。Boolean多項式専用のデータ構造やアルゴリズムを持つPolyBoRiなどを使えば条件は変わりますが、この章では実行していません。

辞書式順序の基底から盤面を戻す¶

groebner には、有理数係数を表す QQ と辞書式順序 lex を指定します。計算結果は、入力と同じ共通解を持つ、一定の形に整理されたGröbner基底です。Boolean方程式によって各変数が0か1に限られるため、調べる共通解は有限個です。基底を生成する多項式全体という代数的な見方は、前の補足で述べたイデアルに対応します。

SymPyの solve_poly_system に基底を渡し、各変数の値を厳密に求めます。strict=True は、不完全になると分かっている解を黙って返さず、例外にする指定です [1]。今回の根はBoolean方程式によって0か1に限られるため、得た全ての根を盤面へ戻せます。最後に共通検証器で初期配置、行、列、ブロックを検査します。

def solve(givens: Board) -> SolveResult:
    model = build_polynomial_model(givens)

    if not model.variables:
        valid, _ = validate_solution(givens, givens)
        return SolveResult(
            status="solved" if valid else "unsat",
            variables=0,
            input_polynomials=len(model.polynomials),
            basis=() if valid else (Integer(1),),
            solutions=(givens,) if valid else (),
        )

    # 辞書式順序の被約Gröbner基底を、有理数係数で正確に計算する。
    computed = groebner(
        model.polynomials,
        *model.variables,
        order="lex",
        domain=QQ,
    )
    basis = tuple(polynomial.as_expr() for polynomial in computed.polys)

    # 基底が[1]なら連立方程式は1 = 0を含み、共通解を持たない。
    if basis == (Integer(1),):
        return SolveResult(
            status="unsat",
            variables=len(model.variables),
            input_polynomials=len(model.polynomials),
            basis=basis,
            solutions=(),
        )

    # Boolean方程式を含む零次元系なので、基底から全ての根を厳密に求める。
    roots = solve_poly_system(
        basis,
        *model.variables,
        strict=True,
    )
    if roots is None:
        raise ValueError("Gröbner基底から解を復元できません")

    solutions: set[Board] = set()
    for root in roots:
        if any(value not in (0, 1) for value in root):
            raise ValueError("Boolean方程式に0、1以外の根が返されました")
        board = decode_solution(model, root)
        valid, errors = validate_solution(board, givens)
        if not valid:
            raise ValueError("共通検証器が完成盤面を拒否しました: " + "; ".join(errors))
        solutions.add(board)

    return SolveResult(
        status="solved" if solutions else "unsat",
        variables=len(model.variables),
        input_polynomials=len(model.polynomials),
        basis=basis,
        solutions=tuple(sorted(solutions)),
    )

基底が単一の定数多項式 \(1\) となる状態は、矛盾方程式 \(1=0\) の存在を示します。これは共通解空間が空集合であることを意味し、unsat と判定します。

実行と検証¶

モデルの実行および検証手順については examples/15-groebner-basis/README.md を参照してください。

通常問題¶

24変数と72本の入力方程式から計算されたグレブナー基底においては、各変数に対する1次式（例: \(x_{1,2,2} - 1 = 0\) や \(x_{2,1,2} = 0\)）が得られ、各マスの数字の選択が直接的に定まります。全根を復元した結果が1盤面のみとなることから一意解であることが判定されます。

解が複数ある問題¶

複数解問題では、基底の末尾に \(x^2 - x = 0\) のような2次式が現れ、変数が0と1の2通りの値を取り得る分岐状態を示します。すべての解を復元した結果、相異なる2つの完成盤面が得られ、本問題の解数がちょうど2であることが確定します。

解がない問題¶

矛盾問題では、多項式イデアルの簡約化により単一の定数多項式基底 [1] （すなわち \(1 = 0\) の矛盾方程式）が得られます。これは連立多項式系に共通解が存在しないことを意味し、解なし（unsat）と確定します。

この方法で分かること¶

基底計算と根の復元が完了すれば、この実装は近似値や乱数を使わずに全解を得ます。解が0個なら unsat、1個なら一意解、2個以上なら複数解です。掲載した三問では、盤面と多項式解が対応することを共通検証器でも確認しました。

unsat や一意性の判定には、基底計算と根の復元を最後まで完了する必要があります。掲載コードは時間制限や unknown を返す仕組みを持たず、基底計算が終わるまで待ちます。

Gröbner基底は、数独専用の解法ではありません。多項式で表した暗号、論理回路、形式検証などにも応用されています。Boolean多項式へ特化した処理系では、その構造に合わせたデータ表現も使われます [3]。この章の数独は、組合せ規則を多項式へ移し、代数計算で全解や矛盾を取り出す小さな例です。

参考文献¶

[1] (1,2)

SymPy Development Team. SymPy 1.14.0 Documentation: Polynomials Manipulation Module Reference and Polynomial System Solvers. SymPy, 2026. Accessed 2026-08-09. URL: https://docs.sympy.org/latest/modules/polys/reference.html#sympy.polys.polytools.groebner.

[2] (1,2)

Elizabeth Arnold, Stephen Lucas, and Laura Taalman. Gröbner Basis Representations of Sudoku. The College Mathematics Journal, 41(2):101–112, 2010. URL: https://educ.jmu.edu/~arnoldea/cmjarnoldlucastaalman.pdf, doi:10.4169/074683410X480203.

[3] (1,2)

Michael Brickenstein and Alexander Dreyer. PolyBoRi: A Framework for Gröbner-Basis Computations with Boolean Polynomials. Journal of Symbolic Computation, 44(9):1326–1345, 2009. URL: https://polybori.sourceforge.net/, doi:10.1016/j.jsc.2008.02.017.