ひとりにしてくれが好きだ

z3pyを導入しましたよ、というだけの日記です。
相も変わらず、「ひとりにしてくれ」の数字埋めを扱います。

処置前サンプル。これを、

こんなふうにしたい。

pythonを触ったこともほぼないので、配列すら使わずにベタ書きしてしまいます。

# モジュールをインポートする
from z3 import *

# 変数を用意する
aaa_00_00 = Int('aaa_00_00')
aaa_01_00 = Int('aaa_01_00')
aaa_02_00 = Int('aaa_02_00')
aaa_03_00 = Int('aaa_03_00')
aaa_04_00 = Int('aaa_04_00')
aaa_05_00 = Int('aaa_05_00')
aaa_06_00 = Int('aaa_06_00')
aaa_07_00 = Int('aaa_07_00')
aaa_00_01 = Int('aaa_00_01')
aaa_01_01 = Int('aaa_01_01')
...（中略）...
aaa_07_07 = Int('aaa_07_07')

solver = Solver()

# 変数は１以上８以下
solver.add( aaa_00_00 > 0, aaa_00_00 < 9)
solver.add( aaa_01_00 > 0, aaa_01_00 < 9)
...（中略）...
solver.add( aaa_07_07 > 0, aaa_07_07 < 9)

# 各マスの関係の制約を記述
solver.add( aaa_00_00 == aaa_01_00 )
solver.add( aaa_00_00 == aaa_02_00 )
solver.add( aaa_00_00 != aaa_03_00 )
solver.add( aaa_00_00 != aaa_04_00 )
...（中略）...
solver.add( aaa_07_03 != aaa_07_07 )
solver.add( aaa_07_04 == aaa_07_05 )
solver.add( aaa_07_04 != aaa_07_06 )
solver.add( aaa_07_04 != aaa_07_07 )
solver.add( aaa_07_05 != aaa_07_06 )
solver.add( aaa_07_05 != aaa_07_07 )
solver.add( aaa_07_06 != aaa_07_07 )

# 解いておくれ
print(solver.check())
print(solver.model())

パッと見で把握しやすいように、雑に略しましたけどわかりますよね。
各マスの関係ですが、縦横に見て、２つのマスの組み合わせに関して、両方数字が入っていて等しいならイコール、そうでなければノットイコールで結ぶだけです。

結果はこんな感じ。

sat
[aaa_07_03 = 2,
aaa_01_01 = 2,
aaa_01_05 = 4,
aaa_01_02 = 5,
aaa_00_06 = 3,

... (中略) ...
aaa_01_00 = 7,
aaa_02_00 = 7]

結果を得てしまえば、あとは適切なスクリプトを書いてパズル盤面として成形するだけです。今回の場合はawkを使用してpenilboxの形式に変換しました。

重い腰を上げて使ってみたけど、導入は簡単だし、そりゃ使われるよねpythonってところ。
やりたいことは伝えられてるんじゃないかと思うので、どなたかもっと便利に洗練された形に仕上げてくれると幸いです。
ということでレッツエンジョイひとくれライフ！

以下ソースコードとかいろいろ。

穴埋め前のひとりにしてくれpencilbox fileサンプル

8
8
1 1 1 0 4 0 0 0
0 0 0 2 2 3 0 3
0 3 0 2 2 0 0 0
4 3 4 0 0 4 0 0
0 3 0 0 4 0 5 5
4 0 4 0 0 0 5 5
0 1 0 7 6 6 0 0
8 0 0 7 6 6 0 8
# + # + + + + +
+ + + + # + + #
+ # + # + + + +
+ + # + + # + +
+ # + + # + # +
# + + + + + + #
+ # + # + # + +
+ + + + # + + #

pencilbox形式→pythonに食わせるスクリプト、変換awkスクリプト

{
 if(NR==1){
  ymax = $1;
 }else if(NR==2){
  xmax = $1;
 }else if(NR<ymax+3){
  j = NR - 3;
  for(i=0;i<xmax;i++){
   aaa[j*xmax+i] = $(i+1);
  }
 }
}
END{
 print "from z3 import *";

 for(j=0;j<ymax;j++){
  for(i=0;i<xmax;i++){
   printf("aaa_%02d_%02d = Int('aaa_%02d_%02d')\n",i,j,i,j);
  }
 }

 print "solver = Solver()";

 for(j=0;j<ymax;j++){
  for(i=0;i<xmax;i++){
   printf("solver.add( aaa_%02d_%02d > 0, aaa_%02d_%02d < 9)\n",i,j,i,j);
  }
 }

 printf "\n";

 for(j=0;j<ymax;j++){
  for(i=0;i<xmax;i++){
   for(ii=i+1;ii<xmax;ii++){
    num_a = aaa[j*xmax+i];
    num_b = aaa[j*xmax+ii];
    if(( num_a * num_b !=0 )&&( num_a == num_b ) ){
     printf("solver.add( aaa_%02d_%02d == aaa_%02d_%02d )\n",i,j,ii,j);
    }else{
     printf("solver.add( aaa_%02d_%02d != aaa_%02d_%02d )\n",i,j,ii,j);
    }
   }
  }
 }

  for(i=0;i<xmax;i++){
 for(j=0;j<ymax;j++){
   for(jj=j+1;jj<ymax;jj++){
    num_a = aaa[j*xmax+i];
    num_b = aaa[jj*xmax+i];
    if(( num_a * num_b !=0 )&&( num_a == num_b ) ){
     printf("solver.add( aaa_%02d_%02d == aaa_%02d_%02d )\n",i,j,i,jj);
    }else{
     printf("solver.add( aaa_%02d_%02d != aaa_%02d_%02d )\n",i,j,i,jj);
    }
   }
  }
 }
 print "print(solver.check())";
 print "print(solver.model())";
}

Pythonスクリプトぜんぶ

from z3 import *
aaa_00_00 = Int('aaa_00_00')
aaa_01_00 = Int('aaa_01_00')
aaa_02_00 = Int('aaa_02_00')
aaa_03_00 = Int('aaa_03_00')
aaa_04_00 = Int('aaa_04_00')
aaa_05_00 = Int('aaa_05_00')
aaa_06_00 = Int('aaa_06_00')
aaa_07_00 = Int('aaa_07_00')
aaa_00_01 = Int('aaa_00_01')
aaa_01_01 = Int('aaa_01_01')
aaa_02_01 = Int('aaa_02_01')
aaa_03_01 = Int('aaa_03_01')
aaa_04_01 = Int('aaa_04_01')
aaa_05_01 = Int('aaa_05_01')
aaa_06_01 = Int('aaa_06_01')
aaa_07_01 = Int('aaa_07_01')
aaa_00_02 = Int('aaa_00_02')
aaa_01_02 = Int('aaa_01_02')
aaa_02_02 = Int('aaa_02_02')
aaa_03_02 = Int('aaa_03_02')
aaa_04_02 = Int('aaa_04_02')
aaa_05_02 = Int('aaa_05_02')
aaa_06_02 = Int('aaa_06_02')
aaa_07_02 = Int('aaa_07_02')
aaa_00_03 = Int('aaa_00_03')
aaa_01_03 = Int('aaa_01_03')
aaa_02_03 = Int('aaa_02_03')
aaa_03_03 = Int('aaa_03_03')
aaa_04_03 = Int('aaa_04_03')
aaa_05_03 = Int('aaa_05_03')
aaa_06_03 = Int('aaa_06_03')
aaa_07_03 = Int('aaa_07_03')
aaa_00_04 = Int('aaa_00_04')
aaa_01_04 = Int('aaa_01_04')
aaa_02_04 = Int('aaa_02_04')
aaa_03_04 = Int('aaa_03_04')
aaa_04_04 = Int('aaa_04_04')
aaa_05_04 = Int('aaa_05_04')
aaa_06_04 = Int('aaa_06_04')
aaa_07_04 = Int('aaa_07_04')
aaa_00_05 = Int('aaa_00_05')
aaa_01_05 = Int('aaa_01_05')
aaa_02_05 = Int('aaa_02_05')
aaa_03_05 = Int('aaa_03_05')
aaa_04_05 = Int('aaa_04_05')
aaa_05_05 = Int('aaa_05_05')
aaa_06_05 = Int('aaa_06_05')
aaa_07_05 = Int('aaa_07_05')
aaa_00_06 = Int('aaa_00_06')
aaa_01_06 = Int('aaa_01_06')
aaa_02_06 = Int('aaa_02_06')
aaa_03_06 = Int('aaa_03_06')
aaa_04_06 = Int('aaa_04_06')
aaa_05_06 = Int('aaa_05_06')
aaa_06_06 = Int('aaa_06_06')
aaa_07_06 = Int('aaa_07_06')
aaa_00_07 = Int('aaa_00_07')
aaa_01_07 = Int('aaa_01_07')
aaa_02_07 = Int('aaa_02_07')
aaa_03_07 = Int('aaa_03_07')
aaa_04_07 = Int('aaa_04_07')
aaa_05_07 = Int('aaa_05_07')
aaa_06_07 = Int('aaa_06_07')
aaa_07_07 = Int('aaa_07_07')
solver = Solver()
solver.add( aaa_00_00 > 0, aaa_00_00 < 9)
solver.add( aaa_01_00 > 0, aaa_01_00 < 9)
solver.add( aaa_02_00 > 0, aaa_02_00 < 9)
solver.add( aaa_03_00 > 0, aaa_03_00 < 9)
solver.add( aaa_04_00 > 0, aaa_04_00 < 9)
solver.add( aaa_05_00 > 0, aaa_05_00 < 9)
solver.add( aaa_06_00 > 0, aaa_06_00 < 9)
solver.add( aaa_07_00 > 0, aaa_07_00 < 9)
solver.add( aaa_00_01 > 0, aaa_00_01 < 9)
solver.add( aaa_01_01 > 0, aaa_01_01 < 9)
solver.add( aaa_02_01 > 0, aaa_02_01 < 9)
solver.add( aaa_03_01 > 0, aaa_03_01 < 9)
solver.add( aaa_04_01 > 0, aaa_04_01 < 9)
solver.add( aaa_05_01 > 0, aaa_05_01 < 9)
solver.add( aaa_06_01 > 0, aaa_06_01 < 9)
solver.add( aaa_07_01 > 0, aaa_07_01 < 9)
solver.add( aaa_00_02 > 0, aaa_00_02 < 9)
solver.add( aaa_01_02 > 0, aaa_01_02 < 9)
solver.add( aaa_02_02 > 0, aaa_02_02 < 9)
solver.add( aaa_03_02 > 0, aaa_03_02 < 9)
solver.add( aaa_04_02 > 0, aaa_04_02 < 9)
solver.add( aaa_05_02 > 0, aaa_05_02 < 9)
solver.add( aaa_06_02 > 0, aaa_06_02 < 9)
solver.add( aaa_07_02 > 0, aaa_07_02 < 9)
solver.add( aaa_00_03 > 0, aaa_00_03 < 9)
solver.add( aaa_01_03 > 0, aaa_01_03 < 9)
solver.add( aaa_02_03 > 0, aaa_02_03 < 9)
solver.add( aaa_03_03 > 0, aaa_03_03 < 9)
solver.add( aaa_04_03 > 0, aaa_04_03 < 9)
solver.add( aaa_05_03 > 0, aaa_05_03 < 9)
solver.add( aaa_06_03 > 0, aaa_06_03 < 9)
solver.add( aaa_07_03 > 0, aaa_07_03 < 9)
solver.add( aaa_00_04 > 0, aaa_00_04 < 9)
solver.add( aaa_01_04 > 0, aaa_01_04 < 9)
solver.add( aaa_02_04 > 0, aaa_02_04 < 9)
solver.add( aaa_03_04 > 0, aaa_03_04 < 9)
solver.add( aaa_04_04 > 0, aaa_04_04 < 9)
solver.add( aaa_05_04 > 0, aaa_05_04 < 9)
solver.add( aaa_06_04 > 0, aaa_06_04 < 9)
solver.add( aaa_07_04 > 0, aaa_07_04 < 9)
solver.add( aaa_00_05 > 0, aaa_00_05 < 9)
solver.add( aaa_01_05 > 0, aaa_01_05 < 9)
solver.add( aaa_02_05 > 0, aaa_02_05 < 9)
solver.add( aaa_03_05 > 0, aaa_03_05 < 9)
solver.add( aaa_04_05 > 0, aaa_04_05 < 9)
solver.add( aaa_05_05 > 0, aaa_05_05 < 9)
solver.add( aaa_06_05 > 0, aaa_06_05 < 9)
solver.add( aaa_07_05 > 0, aaa_07_05 < 9)
solver.add( aaa_00_06 > 0, aaa_00_06 < 9)
solver.add( aaa_01_06 > 0, aaa_01_06 < 9)
solver.add( aaa_02_06 > 0, aaa_02_06 < 9)
solver.add( aaa_03_06 > 0, aaa_03_06 < 9)
solver.add( aaa_04_06 > 0, aaa_04_06 < 9)
solver.add( aaa_05_06 > 0, aaa_05_06 < 9)
solver.add( aaa_06_06 > 0, aaa_06_06 < 9)
solver.add( aaa_07_06 > 0, aaa_07_06 < 9)
solver.add( aaa_00_07 > 0, aaa_00_07 < 9)
solver.add( aaa_01_07 > 0, aaa_01_07 < 9)
solver.add( aaa_02_07 > 0, aaa_02_07 < 9)
solver.add( aaa_03_07 > 0, aaa_03_07 < 9)
solver.add( aaa_04_07 > 0, aaa_04_07 < 9)
solver.add( aaa_05_07 > 0, aaa_05_07 < 9)
solver.add( aaa_06_07 > 0, aaa_06_07 < 9)
solver.add( aaa_07_07 > 0, aaa_07_07 < 9)

solver.add( aaa_00_00 == aaa_01_00 )
solver.add( aaa_00_00 == aaa_02_00 )
solver.add( aaa_00_00 != aaa_03_00 )
solver.add( aaa_00_00 != aaa_04_00 )
solver.add( aaa_00_00 != aaa_05_00 )
solver.add( aaa_00_00 != aaa_06_00 )
solver.add( aaa_00_00 != aaa_07_00 )
solver.add( aaa_01_00 == aaa_02_00 )
solver.add( aaa_01_00 != aaa_03_00 )
solver.add( aaa_01_00 != aaa_04_00 )
solver.add( aaa_01_00 != aaa_05_00 )
solver.add( aaa_01_00 != aaa_06_00 )
solver.add( aaa_01_00 != aaa_07_00 )
solver.add( aaa_02_00 != aaa_03_00 )
solver.add( aaa_02_00 != aaa_04_00 )
solver.add( aaa_02_00 != aaa_05_00 )
solver.add( aaa_02_00 != aaa_06_00 )
solver.add( aaa_02_00 != aaa_07_00 )
solver.add( aaa_03_00 != aaa_04_00 )
solver.add( aaa_03_00 != aaa_05_00 )
solver.add( aaa_03_00 != aaa_06_00 )
solver.add( aaa_03_00 != aaa_07_00 )
solver.add( aaa_04_00 != aaa_05_00 )
solver.add( aaa_04_00 != aaa_06_00 )
solver.add( aaa_04_00 != aaa_07_00 )
solver.add( aaa_05_00 != aaa_06_00 )
solver.add( aaa_05_00 != aaa_07_00 )
solver.add( aaa_06_00 != aaa_07_00 )
solver.add( aaa_00_01 != aaa_01_01 )
solver.add( aaa_00_01 != aaa_02_01 )
solver.add( aaa_00_01 != aaa_03_01 )
solver.add( aaa_00_01 != aaa_04_01 )
solver.add( aaa_00_01 != aaa_05_01 )
solver.add( aaa_00_01 != aaa_06_01 )
solver.add( aaa_00_01 != aaa_07_01 )
solver.add( aaa_01_01 != aaa_02_01 )
solver.add( aaa_01_01 != aaa_03_01 )
solver.add( aaa_01_01 != aaa_04_01 )
solver.add( aaa_01_01 != aaa_05_01 )
solver.add( aaa_01_01 != aaa_06_01 )
solver.add( aaa_01_01 != aaa_07_01 )
solver.add( aaa_02_01 != aaa_03_01 )
solver.add( aaa_02_01 != aaa_04_01 )
solver.add( aaa_02_01 != aaa_05_01 )
solver.add( aaa_02_01 != aaa_06_01 )
solver.add( aaa_02_01 != aaa_07_01 )
solver.add( aaa_03_01 == aaa_04_01 )
solver.add( aaa_03_01 != aaa_05_01 )
solver.add( aaa_03_01 != aaa_06_01 )
solver.add( aaa_03_01 != aaa_07_01 )
solver.add( aaa_04_01 != aaa_05_01 )
solver.add( aaa_04_01 != aaa_06_01 )
solver.add( aaa_04_01 != aaa_07_01 )
solver.add( aaa_05_01 != aaa_06_01 )
solver.add( aaa_05_01 == aaa_07_01 )
solver.add( aaa_06_01 != aaa_07_01 )
solver.add( aaa_00_02 != aaa_01_02 )
solver.add( aaa_00_02 != aaa_02_02 )
solver.add( aaa_00_02 != aaa_03_02 )
solver.add( aaa_00_02 != aaa_04_02 )
solver.add( aaa_00_02 != aaa_05_02 )
solver.add( aaa_00_02 != aaa_06_02 )
solver.add( aaa_00_02 != aaa_07_02 )
solver.add( aaa_01_02 != aaa_02_02 )
solver.add( aaa_01_02 != aaa_03_02 )
solver.add( aaa_01_02 != aaa_04_02 )
solver.add( aaa_01_02 != aaa_05_02 )
solver.add( aaa_01_02 != aaa_06_02 )
solver.add( aaa_01_02 != aaa_07_02 )
solver.add( aaa_02_02 != aaa_03_02 )
solver.add( aaa_02_02 != aaa_04_02 )
solver.add( aaa_02_02 != aaa_05_02 )
solver.add( aaa_02_02 != aaa_06_02 )
solver.add( aaa_02_02 != aaa_07_02 )
solver.add( aaa_03_02 == aaa_04_02 )
solver.add( aaa_03_02 != aaa_05_02 )
solver.add( aaa_03_02 != aaa_06_02 )
solver.add( aaa_03_02 != aaa_07_02 )
solver.add( aaa_04_02 != aaa_05_02 )
solver.add( aaa_04_02 != aaa_06_02 )
solver.add( aaa_04_02 != aaa_07_02 )
solver.add( aaa_05_02 != aaa_06_02 )
solver.add( aaa_05_02 != aaa_07_02 )
solver.add( aaa_06_02 != aaa_07_02 )
solver.add( aaa_00_03 != aaa_01_03 )
solver.add( aaa_00_03 == aaa_02_03 )
solver.add( aaa_00_03 != aaa_03_03 )
solver.add( aaa_00_03 != aaa_04_03 )
solver.add( aaa_00_03 == aaa_05_03 )
solver.add( aaa_00_03 != aaa_06_03 )
solver.add( aaa_00_03 != aaa_07_03 )
solver.add( aaa_01_03 != aaa_02_03 )
solver.add( aaa_01_03 != aaa_03_03 )
solver.add( aaa_01_03 != aaa_04_03 )
solver.add( aaa_01_03 != aaa_05_03 )
solver.add( aaa_01_03 != aaa_06_03 )
solver.add( aaa_01_03 != aaa_07_03 )
solver.add( aaa_02_03 != aaa_03_03 )
solver.add( aaa_02_03 != aaa_04_03 )
solver.add( aaa_02_03 == aaa_05_03 )
solver.add( aaa_02_03 != aaa_06_03 )
solver.add( aaa_02_03 != aaa_07_03 )
solver.add( aaa_03_03 != aaa_04_03 )
solver.add( aaa_03_03 != aaa_05_03 )
solver.add( aaa_03_03 != aaa_06_03 )
solver.add( aaa_03_03 != aaa_07_03 )
solver.add( aaa_04_03 != aaa_05_03 )
solver.add( aaa_04_03 != aaa_06_03 )
solver.add( aaa_04_03 != aaa_07_03 )
solver.add( aaa_05_03 != aaa_06_03 )
solver.add( aaa_05_03 != aaa_07_03 )
solver.add( aaa_06_03 != aaa_07_03 )
solver.add( aaa_00_04 != aaa_01_04 )
solver.add( aaa_00_04 != aaa_02_04 )
solver.add( aaa_00_04 != aaa_03_04 )
solver.add( aaa_00_04 != aaa_04_04 )
solver.add( aaa_00_04 != aaa_05_04 )
solver.add( aaa_00_04 != aaa_06_04 )
solver.add( aaa_00_04 != aaa_07_04 )
solver.add( aaa_01_04 != aaa_02_04 )
solver.add( aaa_01_04 != aaa_03_04 )
solver.add( aaa_01_04 != aaa_04_04 )
solver.add( aaa_01_04 != aaa_05_04 )
solver.add( aaa_01_04 != aaa_06_04 )
solver.add( aaa_01_04 != aaa_07_04 )
solver.add( aaa_02_04 != aaa_03_04 )
solver.add( aaa_02_04 != aaa_04_04 )
solver.add( aaa_02_04 != aaa_05_04 )
solver.add( aaa_02_04 != aaa_06_04 )
solver.add( aaa_02_04 != aaa_07_04 )
solver.add( aaa_03_04 != aaa_04_04 )
solver.add( aaa_03_04 != aaa_05_04 )
solver.add( aaa_03_04 != aaa_06_04 )
solver.add( aaa_03_04 != aaa_07_04 )
solver.add( aaa_04_04 != aaa_05_04 )
solver.add( aaa_04_04 != aaa_06_04 )
solver.add( aaa_04_04 != aaa_07_04 )
solver.add( aaa_05_04 != aaa_06_04 )
solver.add( aaa_05_04 != aaa_07_04 )
solver.add( aaa_06_04 == aaa_07_04 )
solver.add( aaa_00_05 != aaa_01_05 )
solver.add( aaa_00_05 == aaa_02_05 )
solver.add( aaa_00_05 != aaa_03_05 )
solver.add( aaa_00_05 != aaa_04_05 )
solver.add( aaa_00_05 != aaa_05_05 )
solver.add( aaa_00_05 != aaa_06_05 )
solver.add( aaa_00_05 != aaa_07_05 )
solver.add( aaa_01_05 != aaa_02_05 )
solver.add( aaa_01_05 != aaa_03_05 )
solver.add( aaa_01_05 != aaa_04_05 )
solver.add( aaa_01_05 != aaa_05_05 )
solver.add( aaa_01_05 != aaa_06_05 )
solver.add( aaa_01_05 != aaa_07_05 )
solver.add( aaa_02_05 != aaa_03_05 )
solver.add( aaa_02_05 != aaa_04_05 )
solver.add( aaa_02_05 != aaa_05_05 )
solver.add( aaa_02_05 != aaa_06_05 )
solver.add( aaa_02_05 != aaa_07_05 )
solver.add( aaa_03_05 != aaa_04_05 )
solver.add( aaa_03_05 != aaa_05_05 )
solver.add( aaa_03_05 != aaa_06_05 )
solver.add( aaa_03_05 != aaa_07_05 )
solver.add( aaa_04_05 != aaa_05_05 )
solver.add( aaa_04_05 != aaa_06_05 )
solver.add( aaa_04_05 != aaa_07_05 )
solver.add( aaa_05_05 != aaa_06_05 )
solver.add( aaa_05_05 != aaa_07_05 )
solver.add( aaa_06_05 == aaa_07_05 )
solver.add( aaa_00_06 != aaa_01_06 )
solver.add( aaa_00_06 != aaa_02_06 )
solver.add( aaa_00_06 != aaa_03_06 )
solver.add( aaa_00_06 != aaa_04_06 )
solver.add( aaa_00_06 != aaa_05_06 )
solver.add( aaa_00_06 != aaa_06_06 )
solver.add( aaa_00_06 != aaa_07_06 )
solver.add( aaa_01_06 != aaa_02_06 )
solver.add( aaa_01_06 != aaa_03_06 )
solver.add( aaa_01_06 != aaa_04_06 )
solver.add( aaa_01_06 != aaa_05_06 )
solver.add( aaa_01_06 != aaa_06_06 )
solver.add( aaa_01_06 != aaa_07_06 )
solver.add( aaa_02_06 != aaa_03_06 )
solver.add( aaa_02_06 != aaa_04_06 )
solver.add( aaa_02_06 != aaa_05_06 )
solver.add( aaa_02_06 != aaa_06_06 )
solver.add( aaa_02_06 != aaa_07_06 )
solver.add( aaa_03_06 != aaa_04_06 )
solver.add( aaa_03_06 != aaa_05_06 )
solver.add( aaa_03_06 != aaa_06_06 )
solver.add( aaa_03_06 != aaa_07_06 )
solver.add( aaa_04_06 == aaa_05_06 )
solver.add( aaa_04_06 != aaa_06_06 )
solver.add( aaa_04_06 != aaa_07_06 )
solver.add( aaa_05_06 != aaa_06_06 )
solver.add( aaa_05_06 != aaa_07_06 )
solver.add( aaa_06_06 != aaa_07_06 )
solver.add( aaa_00_07 != aaa_01_07 )
solver.add( aaa_00_07 != aaa_02_07 )
solver.add( aaa_00_07 != aaa_03_07 )
solver.add( aaa_00_07 != aaa_04_07 )
solver.add( aaa_00_07 != aaa_05_07 )
solver.add( aaa_00_07 != aaa_06_07 )
solver.add( aaa_00_07 == aaa_07_07 )
solver.add( aaa_01_07 != aaa_02_07 )
solver.add( aaa_01_07 != aaa_03_07 )
solver.add( aaa_01_07 != aaa_04_07 )
solver.add( aaa_01_07 != aaa_05_07 )
solver.add( aaa_01_07 != aaa_06_07 )
solver.add( aaa_01_07 != aaa_07_07 )
solver.add( aaa_02_07 != aaa_03_07 )
solver.add( aaa_02_07 != aaa_04_07 )
solver.add( aaa_02_07 != aaa_05_07 )
solver.add( aaa_02_07 != aaa_06_07 )
solver.add( aaa_02_07 != aaa_07_07 )
solver.add( aaa_03_07 != aaa_04_07 )
solver.add( aaa_03_07 != aaa_05_07 )
solver.add( aaa_03_07 != aaa_06_07 )
solver.add( aaa_03_07 != aaa_07_07 )
solver.add( aaa_04_07 == aaa_05_07 )
solver.add( aaa_04_07 != aaa_06_07 )
solver.add( aaa_04_07 != aaa_07_07 )
solver.add( aaa_05_07 != aaa_06_07 )
solver.add( aaa_05_07 != aaa_07_07 )
solver.add( aaa_06_07 != aaa_07_07 )
solver.add( aaa_00_00 != aaa_00_01 )
solver.add( aaa_00_00 != aaa_00_02 )
solver.add( aaa_00_00 != aaa_00_03 )
solver.add( aaa_00_00 != aaa_00_04 )
solver.add( aaa_00_00 != aaa_00_05 )
solver.add( aaa_00_00 != aaa_00_06 )
solver.add( aaa_00_00 != aaa_00_07 )
solver.add( aaa_00_01 != aaa_00_02 )
solver.add( aaa_00_01 != aaa_00_03 )
solver.add( aaa_00_01 != aaa_00_04 )
solver.add( aaa_00_01 != aaa_00_05 )
solver.add( aaa_00_01 != aaa_00_06 )
solver.add( aaa_00_01 != aaa_00_07 )
solver.add( aaa_00_02 != aaa_00_03 )
solver.add( aaa_00_02 != aaa_00_04 )
solver.add( aaa_00_02 != aaa_00_05 )
solver.add( aaa_00_02 != aaa_00_06 )
solver.add( aaa_00_02 != aaa_00_07 )
solver.add( aaa_00_03 != aaa_00_04 )
solver.add( aaa_00_03 == aaa_00_05 )
solver.add( aaa_00_03 != aaa_00_06 )
solver.add( aaa_00_03 != aaa_00_07 )
solver.add( aaa_00_04 != aaa_00_05 )
solver.add( aaa_00_04 != aaa_00_06 )
solver.add( aaa_00_04 != aaa_00_07 )
solver.add( aaa_00_05 != aaa_00_06 )
solver.add( aaa_00_05 != aaa_00_07 )
solver.add( aaa_00_06 != aaa_00_07 )
solver.add( aaa_01_00 != aaa_01_01 )
solver.add( aaa_01_00 != aaa_01_02 )
solver.add( aaa_01_00 != aaa_01_03 )
solver.add( aaa_01_00 != aaa_01_04 )
solver.add( aaa_01_00 != aaa_01_05 )
solver.add( aaa_01_00 == aaa_01_06 )
solver.add( aaa_01_00 != aaa_01_07 )
solver.add( aaa_01_01 != aaa_01_02 )
solver.add( aaa_01_01 != aaa_01_03 )
solver.add( aaa_01_01 != aaa_01_04 )
solver.add( aaa_01_01 != aaa_01_05 )
solver.add( aaa_01_01 != aaa_01_06 )
solver.add( aaa_01_01 != aaa_01_07 )
solver.add( aaa_01_02 == aaa_01_03 )
solver.add( aaa_01_02 == aaa_01_04 )
solver.add( aaa_01_02 != aaa_01_05 )
solver.add( aaa_01_02 != aaa_01_06 )
solver.add( aaa_01_02 != aaa_01_07 )
solver.add( aaa_01_03 == aaa_01_04 )
solver.add( aaa_01_03 != aaa_01_05 )
solver.add( aaa_01_03 != aaa_01_06 )
solver.add( aaa_01_03 != aaa_01_07 )
solver.add( aaa_01_04 != aaa_01_05 )
solver.add( aaa_01_04 != aaa_01_06 )
solver.add( aaa_01_04 != aaa_01_07 )
solver.add( aaa_01_05 != aaa_01_06 )
solver.add( aaa_01_05 != aaa_01_07 )
solver.add( aaa_01_06 != aaa_01_07 )
solver.add( aaa_02_00 != aaa_02_01 )
solver.add( aaa_02_00 != aaa_02_02 )
solver.add( aaa_02_00 != aaa_02_03 )
solver.add( aaa_02_00 != aaa_02_04 )
solver.add( aaa_02_00 != aaa_02_05 )
solver.add( aaa_02_00 != aaa_02_06 )
solver.add( aaa_02_00 != aaa_02_07 )
solver.add( aaa_02_01 != aaa_02_02 )
solver.add( aaa_02_01 != aaa_02_03 )
solver.add( aaa_02_01 != aaa_02_04 )
solver.add( aaa_02_01 != aaa_02_05 )
solver.add( aaa_02_01 != aaa_02_06 )
solver.add( aaa_02_01 != aaa_02_07 )
solver.add( aaa_02_02 != aaa_02_03 )
solver.add( aaa_02_02 != aaa_02_04 )
solver.add( aaa_02_02 != aaa_02_05 )
solver.add( aaa_02_02 != aaa_02_06 )
solver.add( aaa_02_02 != aaa_02_07 )
solver.add( aaa_02_03 != aaa_02_04 )
solver.add( aaa_02_03 == aaa_02_05 )
solver.add( aaa_02_03 != aaa_02_06 )
solver.add( aaa_02_03 != aaa_02_07 )
solver.add( aaa_02_04 != aaa_02_05 )
solver.add( aaa_02_04 != aaa_02_06 )
solver.add( aaa_02_04 != aaa_02_07 )
solver.add( aaa_02_05 != aaa_02_06 )
solver.add( aaa_02_05 != aaa_02_07 )
solver.add( aaa_02_06 != aaa_02_07 )
solver.add( aaa_03_00 != aaa_03_01 )
solver.add( aaa_03_00 != aaa_03_02 )
solver.add( aaa_03_00 != aaa_03_03 )
solver.add( aaa_03_00 != aaa_03_04 )
solver.add( aaa_03_00 != aaa_03_05 )
solver.add( aaa_03_00 != aaa_03_06 )
solver.add( aaa_03_00 != aaa_03_07 )
solver.add( aaa_03_01 == aaa_03_02 )
solver.add( aaa_03_01 != aaa_03_03 )
solver.add( aaa_03_01 != aaa_03_04 )
solver.add( aaa_03_01 != aaa_03_05 )
solver.add( aaa_03_01 != aaa_03_06 )
solver.add( aaa_03_01 != aaa_03_07 )
solver.add( aaa_03_02 != aaa_03_03 )
solver.add( aaa_03_02 != aaa_03_04 )
solver.add( aaa_03_02 != aaa_03_05 )
solver.add( aaa_03_02 != aaa_03_06 )
solver.add( aaa_03_02 != aaa_03_07 )
solver.add( aaa_03_03 != aaa_03_04 )
solver.add( aaa_03_03 != aaa_03_05 )
solver.add( aaa_03_03 != aaa_03_06 )
solver.add( aaa_03_03 != aaa_03_07 )
solver.add( aaa_03_04 != aaa_03_05 )
solver.add( aaa_03_04 != aaa_03_06 )
solver.add( aaa_03_04 != aaa_03_07 )
solver.add( aaa_03_05 != aaa_03_06 )
solver.add( aaa_03_05 != aaa_03_07 )
solver.add( aaa_03_06 == aaa_03_07 )
solver.add( aaa_04_00 != aaa_04_01 )
solver.add( aaa_04_00 != aaa_04_02 )
solver.add( aaa_04_00 != aaa_04_03 )
solver.add( aaa_04_00 == aaa_04_04 )
solver.add( aaa_04_00 != aaa_04_05 )
solver.add( aaa_04_00 != aaa_04_06 )
solver.add( aaa_04_00 != aaa_04_07 )
solver.add( aaa_04_01 == aaa_04_02 )
solver.add( aaa_04_01 != aaa_04_03 )
solver.add( aaa_04_01 != aaa_04_04 )
solver.add( aaa_04_01 != aaa_04_05 )
solver.add( aaa_04_01 != aaa_04_06 )
solver.add( aaa_04_01 != aaa_04_07 )
solver.add( aaa_04_02 != aaa_04_03 )
solver.add( aaa_04_02 != aaa_04_04 )
solver.add( aaa_04_02 != aaa_04_05 )
solver.add( aaa_04_02 != aaa_04_06 )
solver.add( aaa_04_02 != aaa_04_07 )
solver.add( aaa_04_03 != aaa_04_04 )
solver.add( aaa_04_03 != aaa_04_05 )
solver.add( aaa_04_03 != aaa_04_06 )
solver.add( aaa_04_03 != aaa_04_07 )
solver.add( aaa_04_04 != aaa_04_05 )
solver.add( aaa_04_04 != aaa_04_06 )
solver.add( aaa_04_04 != aaa_04_07 )
solver.add( aaa_04_05 != aaa_04_06 )
solver.add( aaa_04_05 != aaa_04_07 )
solver.add( aaa_04_06 == aaa_04_07 )
solver.add( aaa_05_00 != aaa_05_01 )
solver.add( aaa_05_00 != aaa_05_02 )
solver.add( aaa_05_00 != aaa_05_03 )
solver.add( aaa_05_00 != aaa_05_04 )
solver.add( aaa_05_00 != aaa_05_05 )
solver.add( aaa_05_00 != aaa_05_06 )
solver.add( aaa_05_00 != aaa_05_07 )
solver.add( aaa_05_01 != aaa_05_02 )
solver.add( aaa_05_01 != aaa_05_03 )
solver.add( aaa_05_01 != aaa_05_04 )
solver.add( aaa_05_01 != aaa_05_05 )
solver.add( aaa_05_01 != aaa_05_06 )
solver.add( aaa_05_01 != aaa_05_07 )
solver.add( aaa_05_02 != aaa_05_03 )
solver.add( aaa_05_02 != aaa_05_04 )
solver.add( aaa_05_02 != aaa_05_05 )
solver.add( aaa_05_02 != aaa_05_06 )
solver.add( aaa_05_02 != aaa_05_07 )
solver.add( aaa_05_03 != aaa_05_04 )
solver.add( aaa_05_03 != aaa_05_05 )
solver.add( aaa_05_03 != aaa_05_06 )
solver.add( aaa_05_03 != aaa_05_07 )
solver.add( aaa_05_04 != aaa_05_05 )
solver.add( aaa_05_04 != aaa_05_06 )
solver.add( aaa_05_04 != aaa_05_07 )
solver.add( aaa_05_05 != aaa_05_06 )
solver.add( aaa_05_05 != aaa_05_07 )
solver.add( aaa_05_06 == aaa_05_07 )
solver.add( aaa_06_00 != aaa_06_01 )
solver.add( aaa_06_00 != aaa_06_02 )
solver.add( aaa_06_00 != aaa_06_03 )
solver.add( aaa_06_00 != aaa_06_04 )
solver.add( aaa_06_00 != aaa_06_05 )
solver.add( aaa_06_00 != aaa_06_06 )
solver.add( aaa_06_00 != aaa_06_07 )
solver.add( aaa_06_01 != aaa_06_02 )
solver.add( aaa_06_01 != aaa_06_03 )
solver.add( aaa_06_01 != aaa_06_04 )
solver.add( aaa_06_01 != aaa_06_05 )
solver.add( aaa_06_01 != aaa_06_06 )
solver.add( aaa_06_01 != aaa_06_07 )
solver.add( aaa_06_02 != aaa_06_03 )
solver.add( aaa_06_02 != aaa_06_04 )
solver.add( aaa_06_02 != aaa_06_05 )
solver.add( aaa_06_02 != aaa_06_06 )
solver.add( aaa_06_02 != aaa_06_07 )
solver.add( aaa_06_03 != aaa_06_04 )
solver.add( aaa_06_03 != aaa_06_05 )
solver.add( aaa_06_03 != aaa_06_06 )
solver.add( aaa_06_03 != aaa_06_07 )
solver.add( aaa_06_04 == aaa_06_05 )
solver.add( aaa_06_04 != aaa_06_06 )
solver.add( aaa_06_04 != aaa_06_07 )
solver.add( aaa_06_05 != aaa_06_06 )
solver.add( aaa_06_05 != aaa_06_07 )
solver.add( aaa_06_06 != aaa_06_07 )
solver.add( aaa_07_00 != aaa_07_01 )
solver.add( aaa_07_00 != aaa_07_02 )
solver.add( aaa_07_00 != aaa_07_03 )
solver.add( aaa_07_00 != aaa_07_04 )
solver.add( aaa_07_00 != aaa_07_05 )
solver.add( aaa_07_00 != aaa_07_06 )
solver.add( aaa_07_00 != aaa_07_07 )
solver.add( aaa_07_01 != aaa_07_02 )
solver.add( aaa_07_01 != aaa_07_03 )
solver.add( aaa_07_01 != aaa_07_04 )
solver.add( aaa_07_01 != aaa_07_05 )
solver.add( aaa_07_01 != aaa_07_06 )
solver.add( aaa_07_01 != aaa_07_07 )
solver.add( aaa_07_02 != aaa_07_03 )
solver.add( aaa_07_02 != aaa_07_04 )
solver.add( aaa_07_02 != aaa_07_05 )
solver.add( aaa_07_02 != aaa_07_06 )
solver.add( aaa_07_02 != aaa_07_07 )
solver.add( aaa_07_03 != aaa_07_04 )
solver.add( aaa_07_03 != aaa_07_05 )
solver.add( aaa_07_03 != aaa_07_06 )
solver.add( aaa_07_03 != aaa_07_07 )
solver.add( aaa_07_04 == aaa_07_05 )
solver.add( aaa_07_04 != aaa_07_06 )
solver.add( aaa_07_04 != aaa_07_07 )
solver.add( aaa_07_05 != aaa_07_06 )
solver.add( aaa_07_05 != aaa_07_07 )
solver.add( aaa_07_06 != aaa_07_07 )
print(solver.check())
print(solver.model())

結果ぜんぶ

sat
[aaa_07_03 = 2,
aaa_01_01 = 2,
aaa_01_05 = 4,
aaa_01_02 = 5,
aaa_00_06 = 3,
aaa_06_01 = 1,
aaa_03_00 = 4,
aaa_05_02 = 3,
aaa_05_00 = 2,
aaa_07_05 = 3,
aaa_03_07 = 8,
aaa_00_00 = 7,
aaa_06_03 = 8,
aaa_05_07 = 6,
aaa_00_04 = 2,
aaa_07_07 = 4,
aaa_02_01 = 6,
aaa_07_01 = 8,
aaa_07_02 = 6,
aaa_01_07 = 1,
aaa_02_07 = 3,
aaa_02_06 = 5,
aaa_04_02 = 7,
aaa_04_04 = 8,
aaa_06_02 = 4,
aaa_00_01 = 5,
aaa_05_04 = 7,
aaa_06_00 = 6,
aaa_04_03 = 4,
aaa_05_05 = 5,
aaa_07_00 = 5,
aaa_03_04 = 1,
aaa_07_06 = 1,
aaa_02_02 = 2,
aaa_06_07 = 5,
aaa_00_02 = 8,
aaa_02_04 = 4,
aaa_03_03 = 3,
aaa_06_06 = 2,
aaa_03_05 = 6,
aaa_00_03 = 1,
aaa_04_05 = 2,
aaa_04_00 = 8,
aaa_03_06 = 8,
aaa_01_03 = 5,
aaa_01_04 = 5,
aaa_01_06 = 7,
aaa_04_07 = 6,
aaa_00_07 = 4,
aaa_04_06 = 6,
aaa_05_06 = 6,
aaa_06_05 = 3,
aaa_00_05 = 1,
aaa_02_05 = 1,
aaa_06_04 = 3,
aaa_07_04 = 3,
aaa_02_03 = 1,
aaa_05_03 = 1,
aaa_03_02 = 7,
aaa_05_01 = 8,
aaa_03_01 = 7,
aaa_04_01 = 7,
aaa_01_00 = 7,
aaa_02_00 = 7]

結果テキスト→pencilbox形式　変換awkスクリプト

{
 if($0~/aaa/){
  str = $0;
  gsub(/\[/," ",str);
  gsub(/\]/," ",str);
  gsub(/\,/," ",str);
  split(str,tmp);
  aaa[tmp[1]] = tmp[3];
 }
}

END{
 print 8;
 print 8;
 for(j=0;j<8;j++){
  for(i=0;i<8;i++){
   num = sprintf("aaa_%02d_%02d",i,j);
   printf aaa[num] " ";
  }
  printf "\n";
 }
}