akari-sat 0.1.0

Add your description here

Akari Solver

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

必要環境

• Python 3.13 以上
• PySAT

uv add akari-sat

ディレクトリ構成

project/
├── main.py
└── src/
    ├── __init__.py
    └── akari_solver.py

使い方

プロジェクトルートで実行します。

uv run main.py

from src.akari_solver import solve_akari

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

result = solve_akari(H, W, grid)   # 解けない場合は None
if result is not None:
    for r in range(H):
        print("".join("*" if result[r][c] else grid[r][c] for c in range(W)))

入力・出力

入力: grid … 1 行 1 文字列のリスト（list[str]）、または 1 文字ずつの 2 次元配列（list[list[str]]）。各マスの文字は以下の通り。

文字	意味
.	空きマス
#	数字のない壁
0–4	数字付きの壁

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

ルール（エンコード内容）

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

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