PythonでのSATソルバを使って数独パズル（９×９のナンプレ）

var_name_cnf=[] var_name_prefix="p" for i in range(0,9): for j in range(0,9): clause=[] for k in range(1,10): var_name = ger_var_name("+",var_name_prefix,i,j,k) clause.append(var\name) var_name_cnf.append(clause) 今回の作成 １i行j列のマスには１から９のどれか存在する ２i行j列のマスには２つ以上の数字は存在しない ３ 各行・各列・各３×３ブロックに同じ数字は１つしか存在しない ４ヒントで与えられている数字は，該当するマスに存在する． 本題 これの１の部分だけできていると思っているのですが，２の部分を添え字をi，ｊ，a，ｂの４重ループので生成してほしいのと，３の部分を添え字を i，ｊ，ｋ，ｌ，a　の五重ループで作成したサンプルを教えてほしいです．