akari-sat

アカリ（美術館 / Light Up）パズルを SAT ソルバーで解く Python ライブラリです。 盤面のルールを CNF 制約に変換し、PySAT（Glucose3）で求解します。

インストール

pip install akari-sat

uv を使う場合:

uv add akari-sat

使い方

インストール後、akari_sat パッケージから solve_akari を読み込んで使います。

from akari_sat import solve_akari

grid = [
    "..#..",
    "2....",
    "..1..",
    "....0",
    "..#..",
]
H, W = len(grid), len(grid[0])

result = solve_akari(H, W, grid)  # 解が存在しない場合は None

if result is None:
    print("解が見つかりませんでした（充足不能）")
else:
    for r in range(H):
        print("".join("*" if result[r][c] else grid[r][c] for c in range(W)))

実行結果（* が灯り）:

*.#.*
2.*..
*.1..
.*..0
..#*.

API

solve_akari(H, W, grid, solver=Glucose3)

アカリを解きます。

引数:

• H (int): グリッドの高さ。
• W (int): グリッドの幅。
• grid (list[str] | list[list[str]]): 盤面。1 行 1 文字列のリスト、または 1 文字ずつの 2 次元配列で渡します。
• solver: 使用する PySAT のソルバークラス。デフォルトは Glucose3。

戻り値:

• list[list[bool]]: H×W の真偽値の 2 次元配列。result[r][c] が r 行 c 列に灯があるかを表します。
• 解が存在しない場合は None。

各マスの文字の意味:

エンコードしているルール

アカリの 4 つの規則を制約として SAT に与えています。

• 壁・数字マスには灯を置かない。
• 数字マスの上下左右に接する灯の数は、その数字とちょうど一致する。
• 同じ行・列で壁を挟まずに 2 つ以上の灯を置かない（灯どうしは照らし合わない）。
• すべての空きマスがいずれかの灯に照らされる。

動作環境

• Python 3.13 以上
• python-sat（依存パッケージとして自動的に導入されます）

リポジトリ

https://github.com/youseiushida/akari-sat

ライセンス

MIT License