数独オリジナル問題を作成する 4x4から100x100まで


はじめに

スケジュールナースは、組み込みPythonを使って制約する機能があります。この機能を使って、数独オリジナル問題を作成してみます。

pythonコードの解説

pythonコードは、数独サイズ(4-100)間で、同じコードです。GUIの集合情報を組み込んでいるので、短くかつシンプルにpythonコードを書けます。

Sanity チェック

GUIで設定している
1.全日
2.全スタッフ
3.sfiftdef

は、例えば、9x9数独の場合、全て9である必要があります。
また、その平方根は2から、10までがサポート範囲です。

if len(全日) !=len(shiftdef) or len(全日) !=len(全スタッフ):
    raise ValueError("全日 and shiftdef are inconsistent")
blocks=int(math.sqrt(len(全日)))
if math.sqrt(len(全日)) not in range(2,11,1):
    raise ValueError("Illegal sudoku dimmension. Supported sizes are 4x4,9x9...100x100.")

行制約

sc3.xxがスケジュールナース特有の組み込み制約関数です。詳細は、下記マニュアルをご覧ください。
https://www.nurse-scheduling-software.com/tutorial/schedule_nurse3/python_manual/python3_constraint_programming_manual.html

for day in 全日: #column
    for shift in shiftdef.keys():
        V=[]
        for person in 全スタッフ:
            V.append(sc3.GetShiftVar(person,day,shift))
        sc3.AddHard(sc3.SeqLE(1,1,V),'')

列制約

for person in 全スタッフ: #row
    for  shift in shiftdef.keys():
        V=[]
        for  day in 全日:
            V.append(sc3.GetShiftVar(person,day,shift))
        sc3.AddHard(sc3.SeqLE(1,1,V),'')

ブロック制約

for person in range(0,len(全スタッフ),blocks): #block
    for shift in shiftdef.keys():
        for  day in range(0,len(全日),blocks):
            V=[]
            for  i  in range(blocks):
                for  j in range(blocks):
                    V.append(sc3.GetShiftVar(person+i,day+j,shift))
            sc3.AddHard(sc3.SeqLE(1,1,V),'')

と、コンパクトに書けます。

数独問題作成

ブランク数独解を求める

ブランク数独とは、私が勝手に名づけたものです。例えば、4x4数独で、予定をブランクにして2解を求めています。

唯一解であることの証明

この解を予定に送り、再度求解すると、当然のことながら解は、入力した予定そのものしかありません。このとき、2解目は存在しないとのメッセージが出力されます。

言い換えれば、1解しか存在しないということを表しています。つまりこのメッセージが出ているうちは、唯一の解である証明になります。

ブランク部を増やしていく

解が1解しかない間は、ブランクを増やしていけます。
しかし、そのうち、次のように、2解が見つかってしまう場合が出てきますが、これは、数独問題としては、不適です。

少し前に戻って、入力をやり直してもよいですし、諦めて、直前の解を問題として終了でもよいです。
次は、唯一の解しかないので、数独問題として適しています。

サイズを増やす

100x100までやってみました。1時間程度ブランク数独解の生成にかかりました。この辺が限界のようです。

動画

英語版になりますが、動画は以下です。
https://youtu.be/ofCaurpkyJM