数独オリジナル問題を作成する ４ｘ４から１００ｘ１００まで

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

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

##Sanity チェック
GUIで設定している
１．全日
２．全スタッフ
３．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