おおよそ引っ越し完了

荷物の完全移行と元の部屋の掃除を終えて、おおよそ引っ越しが完了しました!

今日は引っ越しでやったことを書いていきたいと思います。

1~2月:引っ越しを考え始めた

彼女との同棲を考えて引っ越しのことを年始くらいに考えはじめました。この頃は様々な賃貸サイトを使って良さそうな物件を紹介しあい、譲れなさそうな条件などを探っている段階でした。

情報共有にはもともと二人用のDiscordサーバがあったので新たに引っ越し用のトピックを作成して、そこに賃貸サイトのURLを貼っていく感じでした。様々な賃貸サイトで調べていて気づいたことは、

  • suumoとathomeはほとんど同じ物件しかない
  • ホームズは物件の写真が豊富
  • yahoo賃貸は他に載っていない物件が結構ある
  • goodroomはおしゃれだが割高な物件が多い

でした。

3月:引っ越しへの意識を高める

この時期にはなんとなくの引越し時期を決めました。この日に引っ越すと決めるというより、おおよそ4月下旬から5月中が良いかなぁという感覚でした。

次に、引っ越しへのイメージを強くするために一度内見に行ってみることにしました。具体的には自分の最寄りの駅前にある不動産屋さん(アパマンショップとかピタットハウスとか)に予約もせず入店し、引越し時期となんとなくの条件を伝えます。

この段階での条件は以下のとおりです。

  • 家賃+管理費が12.5万円以下
  • 各職場へドアトゥードアで50分以内
  • 2階以上
  • 鉄筋コンまたは鉄骨
  • 日当たりがよい(南向き)
  • 1LDK or 2LDK
  • 50平米以上だと尚良(45平米以上は絶対)
  • 角部屋だと尚良

これだけだと、候補が出てきすぎると言われ、不動産屋さんと会話する中でなんとなくの駅も決めました。その場では内見の予定は立てず、条件に合いそうな物件があれば連絡してもらうようにしました。不動産屋さんはもう一店舗くらいまわりました。

そして3月下旬くらいに内見に行きました。

4月:物件決定と引越し準備

4月上旬は興味のある物件を内見しまくりました。全部で6件くらい内見しました。そして4月18日に内見した物件に決定しました🎉。失敗談として、18日より前にも良い物件があったのですが、内見してからすぐに申し込まず優雅に喫茶店でコーヒーを飲んでいたりしたら、次の日に申し込まれたということが2回ほどありました。なので反省を活かし、18日に内見した物件はその日中に書類を用意して入居申請をしました。

そしてここから引っ越しの準備をはじめました。引っ越しでしなければいけないことはTrelloで管理しました。

f:id:makky_emmanuel:20210516085912p:plain

各タスクにはチェックボックスで二人の名前を入れておき、週末になんとなく次の週にやることを今週やることリストに移動しておきました。達成したらチェックをつけ、2つともチェックがついた段階でDONEリストへと移動する感じです。ここではほぼ毎日夜にやることに関する会話ができていたのが良かったのかなぁと思います。

5月:引っ越し

GW中に引っ越し方法や当日することをまとめていきました。私達は業者を頼まず、レンタカーを借りて自分たちで引っ越しすることにしました。具体的にはニコニコレンタカーでミニキャブバンを24時間レンタルしました。費用としては7000円位でした。

また、当日にすることに関してはGoogleスプレッドシートにまとめていきました。

f:id:makky_emmanuel:20210516090815p:plain

そして昨日、互いの元の部屋の掃除をしまして、無事引っ越しを終えることができました。

f:id:makky_emmanuel:20210516091239j:plain

最後に

引っ越し直後で何もないからこそのおしゃれな雰囲気の写真を撮っておきました。

f:id:makky_emmanuel:20210516091212j:plain

GPUを使った機械学習でのデバック

今週のタイムライン

  • Faster R-CNNを勉強した(ほぼ毎日)
  • 引っ越し作業を進めた
  • Core UIを使ってみた(月曜日)
  • リファクタリングした(火曜日)
  • 大学の友達と遊んだ(木曜日)

話したいこと

  1. Faster R-CNNを勉強した(ほぼ毎日)

GPUを使った機械学習

Faster R-CNNを使って物体認識を仕様と勉強中です。環境はGoogle Colab、ライブラリはPytorchを使っています。

Pytorchでは以下のようにdeviceを指定することでGPUで学習や推論処理を行うことができます。

import torchvision

device = torch.device('cuda') if torch.cuda.is_available() else torch.device('cpu') 

model = torchvision.models.detection.fasterrcnn_resnet50_fpn(pretrained=True)
model.to(device)

以下のようにして学習をさせようとしていた時、

torch.manual_seed(1)

dataset = Dataset(BASE_PATH)
n_train = int(len(dataset) * 0.7)
n_val = len(dataset) - n_train
 
train, val = torch.utils.data.random_split(dataset, [n_train, n_val])

def collate_fn(batch):
    return tuple(zip(*batch))

data_loader = torch.utils.data.DataLoader(train, batch_size=2, shuffle=True, collate_fn=collate_fn)

params = [p for p in model.parameters() if p.requires_grad]
optimizer = torch.optim.SGD(params, lr=0.005, momentum=0.9, weight_decay=0.0005)

for i, batch in enumerate(data_loader):
    images, targets = batch

    imagess = [image.to(device) for image in images]
    targets = [{k: v.to(device) for k, v in t.items()} for t in targets]

    pred = model(images, targets)
    losses = sum(loss for loss in pred.values())
    loss_value = losses.item()
    
    optimizer.zero_grad()
    losses.backward()
    optimizer.step()

    if (i+1) % 10 == 0:
        print(f"epoch #{epoch+1} Iteration #{i+1} loss: {loss_value}")  

RuntimeError: CUDA error: device-side assert triggeredが発生してしまいました。より親切なエラーを見るためにはCPUで実行すればよいということを学んだ。

# cpuで実行するように変更
device = torch.device('cpu') 
model.to(device)

for i, batch in enumerate(data_loader):
    images, targets = batch

    imagess = [image.to(device) for image in images]
    targets = [{k: v.to(device) for k, v in t.items()} for t in targets]

    pred = model(images, targets)
    losses = sum(loss for loss in pred.values())
    loss_value = losses.item()
    
    optimizer.zero_grad()
    losses.backward()
    optimizer.step()

    if (i+1) % 10 == 0:
        print(f"epoch #{epoch+1} Iteration #{i+1} loss: {loss_value}")  

そうするとIndexError: Target 6 is out of bounds.ということでfeature mapあたりが間違っていることがわかりました。めでたしめでたし。

今週の思い出

週末にSOLSO FARMに行ってきました。SOLSO FARMは土日祝日だけオープンしているファームマーケットで引越しをしたら何か植物を置きたいなと思い行ってみました。

f:id:makky_emmanuel:20210502080311j:plain f:id:makky_emmanuel:20210502080325j:plain f:id:makky_emmanuel:20210502080335j:plain

知識欲が湧いた週

今週のタイムライン

  • 引っ越しの物件決定(日曜日)
  • Quarkus(月曜日)
  • CNNの応用の勉強(火曜日)
  • Amazon PersonalizeのBatch recommendationを試した(水曜日)
  • A*アルゴリズムをまとめた(金曜日)
  • スープカレーを久々に食べた(土曜日)

話したいこと

  1. CNNの応用の勉強
  2. A*アルゴリズムをまとめた

CNNの応用の勉強

CNN(畳み込みニューラルネットワーク)は様々な分野で使われています。例えば、画像認識(その画像がなんの画像であるかの認識)、人検出など。その中の一つの物体検出を少し勉強しました。

f:id:makky_emmanuel:20210425100840p:plain

上の画像では画像の中のどの部分に何が写っているかがわかります。こういったことをできるようにするのが物体検出です。物体検出は画像認識より難しそうだなということはわかります。

物体検出をできるようにするためには、

  • どの領域(画像の四角)を認識対象とするか
  • 認識対象とした領域の中から認識したいクラス(犬、人、馬など)以外の場所をどうやって排除するか

などの課題を解決すれば良いです。 これらの問題を解決した方法として、R-CNN、Fast R-CNN、Faster R-CNN、YOLO(You Only Look Once)、SDD(Single Shot Multibox Detector)などがあります。

その中で今はR-CNN、Fast R-CNN、Faster R-CNNを勉強中です。Pytorchには様々なモデルが用意されていたり、チュートリアルも豊富です。コツコツ頑張ろう。

pytorch.org

github.com

github.com

A*アルゴリズムをまとめた

経路探索アルゴリズムの一つであるA*アルゴリズムを勉強し直して、理解をまとめました。

勉強する際にWikipedia日本語版英語版で書いてある内容が異なり、それぞれ計算量を減らすための工夫が書いてあってとても興味深かったです。

とりあえず実装はできたので、Wikipediaに書いてある工夫も取り入れてみて高速化できるのか試してみたいなと思います。

最後に

今週は知識欲がとても湧いた週でした。その調子を維持して勉強を進められたらなと思います。

土曜日に、久しぶりにスープカレーを食べました。

f:id:makky_emmanuel:20210425103800j:plain

テストファーストでプログラミング

今週のタイムライン

  • ゴルフの打ちっぱなしに行った(日曜日)
  • 新入社員とドリームマネジメントをやった(月曜日)
  • 新たなAPIを使用した開発のための調査(火曜日)
  • Streamlitを用いたデータ可視化(水曜日)
  • Amazon Personalizeを用いたバッチでの推薦(木曜日)
  • テストファーストでプログラミング(金曜日)

話したいこと

  1. テストファーストでプログラミング

テストファーストでプログラミング

学生の頃とプログラミングをする上で異なるところはテストを書くというところです。品質を担保(ちゃんと動いているかの証明)をするために働く上ではテストコードを書いています。

さらに最近ではテスト駆動開発(あまりわかっていないが)のようにやりたいことや修正したいことを先にテストに書いてしまってから実装を行うということをやっています。

例えば年齢に応じた映画館の料金を算出したいという要望があるとします。仕様は以下の通り。

  • 大人(23歳以上)は1,800円
  • 大学生・専門学生(18歳〜22歳)は1,500円
  • 中学・高校生(13歳〜17歳)は1,000円
  • それ以下は500円 ※細かい料金体系は面倒なので年齢で区切りました

以下のようなクラスを考えるとします。

// PriceCalculator.java
class PriceCalculator {
    static int calculate(int age) {
        return 0;
    }
}

まずやるのは、仕様をテストコードに反映させます。

class PriceCalculatorTest {
    private static final int ADULT_PRICE = 1800;
    private static final int COLLEGE_AND_PROFESSIONAL_STUDENT_PRICE = 1500;
    private static final int SCHOOL_STUDENT_PRICE = 1000;
    private static final int CHILD_PRICE = 500;

    @ParameterizedTest
    @MethodSource
    void shouldReturnValidPrice(int age, int price){
        assertThat(PriceCalculator.calculate(age), is(price));
    }

    static Stream<Arguments> shouldReturnValidPrice() {
        return Stream.of(
                arguments(23, ADULT_PRICE),
                arguments(22, COLLEGE_AND_PROFESSIONAL_STUDENT_PRICE),
                arguments(18, COLLEGE_AND_PROFESSIONAL_STUDENT_PRICE),
                arguments(17, SCHOOL_STUDENT_PRICE),
                arguments(13, SCHOOL_STUDENT_PRICE),
                arguments(12, CHILD_PRICE));
    }
}

このように書いてみると、年齢がマイナスの時や、年齢の上限はどこまで許せば良いんだろうという疑問が湧いてきます。

  • マイナスは例外だよね
  • 最高年齢は現状118歳だから200歳くらいまでを範囲としておいて、それ以上は例外にしちゃおう

などの考慮できていなかった仕様を考えることができます。そしてテストにも追加。

class PriceCalculatorTest {
...

    @ParameterizedTest
    @MethodSource
    void shouldThrow(int age) {
        assertThrows(IllegalArgumentException.class, () -> PriceCalculator.calculate(age));
    }

    static Stream<Arguments> shouldThrow() {
        return Stream.of(
                arguments(201),
                arguments(-1));
    }
}

これでやっと実装しはじめられますね。 こうやってテストファーストで書くのがいいなって思いました。

最後に

人生初の打ちっぱなしに行きました。Youtubeをみてイメージしていきましたが。全然思ったように当たらず。。。新しいことをするのはいつになっても楽しい!

f:id:makky_emmanuel:20210418071613j:plain

社会人3年目開始

今週のタイムライン

エネルギーを与えた出来事(幸せになった・安心した)

  • ドリームマネジメント最終回(月曜日)
  • 機械学習を使って処理速度を改善できた(火曜日)
  • チームメンバーと軽くお酒を飲みながら話せた(水曜日)
  • 社会人3年目開始(木曜日)
  • atCoderを初めてやった(金曜日)

エネルギーを奪った出来事(悲しくなった・不幸になったなど)

特になし

戸惑った出来事や疑問に思った出来事

特になし

話したいこと

  1. 社会人3年目開始
  2. ドリームマネジメント最終回(別記事であげる予定)

社会人3年目開始

2019年に大学院を卒業して、早2年が経ってしまいました。あっという間だったような、よく考えてみると濃かったような。そこで、社会人になってから技術・非技術を問わずにどんな知識に触れてきたのかをバーっと書き出してみました。(趣味的にさっと触れただけのものも入っています)

  • フロント系
    • Typescript, React, Redux, MUI, Nodejs, Jest, TestCafe, Kotlin, Android
  • バック系
    • Java, Spring Boot, JUnit, Mockito, REST Assured
  • インフラ系
    • AWS, Docker, Jenkins, heroku
  • 機械学習アルゴリズム
    • SageMaker, Amazon Personalize
    • LightGBM, XGBoost, k-means, GMM, 経路探索, SAT
    • Pytorch, Keras, Tensolflow.js, pandas
    • Kaggle, SIGNATE
  • その他

こう見ると、いろんなことをやってきたんだなぁと実感。 最近ではアルゴリズム系のことをやるのがとても楽しいです。大学で学んだことが実際に使えたり、ちょっと違った考え方を工夫するだけで処理速度が改善されたりなど知見が結びついていく感じがします。 今年一年も様々なことを学び充実させていくぞー!

最後に

今週はとてもあたたかかったです。月曜日にはきれいな桜を見ましたが、もう散ってしまっているのかな。

f:id:makky_emmanuel:20210403093605j:plain

不安とワクワクの両方を感じる週

今週のタイムライン

エネルギーを与えた出来事(幸せになった・安心した)

  • 仲間の送別会をした(火曜日)
  • MaxSATの勉強をした(火曜日)
  • 経路探索アルゴリズムに興味が出た(木曜日)
  • Search Inside Yourselfを読み始めた(木曜日)
  • スクラムイベントの順番を変えてみた(木曜日)

エネルギーを奪った出来事(悲しくなった・不幸になったなど)

  • 低気圧がすごかった(日曜日)
  • 感情によって自分の行動が変わってしまっていること(水曜日)

戸惑った出来事や疑問に思った出来事

  • Doneにならない前提でプランニング時にアイテムを取ることはどうなんだろうか?(木曜日)

話したいこと

  1. 感情によって自分の行動が変わってしまっていること(水曜日)
  2. 経路探索アルゴリズムに興味が出た(木曜日)

不安になると自分はどうなるか

今週は仕事に対する不安がありながら過ごした週だったなぁと思います。なぜ不安になっていたのか。

その一つは尊敬していた仲間が今月末で転職しいなくなってしまうからです。私はその仲間をとても尊敬していたので、同じようになりたいと思い、一緒に作業する機会を多く作り、知識を吸収してきました。また、半年くらいかけて少し大きなタスクを消化しましたが、その際もその仲間にたくさん相談して、いろいろな問題を解決してきました。そのように頼ってきた部分があったのでいざいなくなるとなるとその仲間が担っていた部分の自分への責任が増え、また相談していた相手であった人もいなくなってしまうため、不安が募ってしまっていました。

また、今週は緊急で対応すべきことが発生しました。その部分に関して一番知識があったのは(転職してしまう仲間をのぞいて)私だったので、どのように解決すべきか、間に合うのかなどさまざまな不安が押し寄せてきました。

そこで今週改めて気づいたのは、私は不安になると「殻に閉じこもってしまうタイプ」なのだなぁ感じました。多分私は責任感が強い方で、どうにかして自分がやらないとと考えてしまうところがあるようです。(逆にいうと人を頼れていないんですが…)なので自分の作業に没頭したいや時間をかけてでもいいからどうにか解決したいという気持ちが強く現れ、思いやりにかけた発言や生活リズムを崩しての作業をしがちです。なんかこの部分は昔から成長していないなぁと感じました。

ブログを書くことで、こうやって自分の感情を振り返るのも面白いなぁと感じたという話でした。 (なんか締めがわからなくなりました笑)

経路探索アルゴリズムに興味が出た

今週は扱っているサービスの処理速度に問題があり、なんとか改善せねばという事態になってバタバタしていました。 いろいろ調査した結果、ある2点間の経路の距離を算出する処理が遅いことに原因がありました。

経路探索は「グラフ上でスタートからゴールまでの道を見つける」というグラフ探索問題として考えることができ、大学時代に習った幅優先探索深さ優先探索などが使うことで解くことができます。また、幅優先探索なんらかの規則に従って次に進むべき道を選ぶようにしたアルゴリズムを最良優先探索といい、このアルゴリズムが経路探索によく使われるアルゴリズムらしいです。

なんらかの規則によってアルゴリズムが変わってきます。

  • ダイクストラ法:スタートからある場所までのコストが最小となるように探索していく。
  • A*アルゴリズム:スタートからある場所までのコスト+推定値が最小となるように探索していく。
  • 均一コスト探索:スタートから通ったところまでのコストの総和が最小となるように探索していく。

A*アルゴリズムはスタートからゴールまでの距離を求める精度は高いのですが、実際にビジネス応用する際には速度の点で課題がありました。そこで他の機械学習アルゴリズムを使って精度は少し下げても良いが、速度をあげようという試みをしようとしています。その中の一つでXGBoostを使おうとしています。XGBoostはKaggleのコンペに挑戦するときに使ったアルゴリズムなのでこんなときに生きてくるとは!今週中盤まで不安がたくさんありましたが、週末になってワクワクが止まらない状況になっています。

最後に

今週は不安がたくさんありましたが、任されることって自分にしかない価値が少しは出てきたのかなと思って良い気分っちゃ良い気分ですね。パームレストを転職してしまう先輩からもらったので、その意思を引き継いでゴリゴリ頑張っていくぞ!

f:id:makky_emmanuel:20210327223401j:plain
もらったパームレスト

SATソルバーで数独を解く

今週のタイムライン

エネルギーを奪った出来事(悲しくなった・不幸になったなど)

  • わからないことをその場で質問できなかった(時間がなかったのもあったが)(水曜日)
  • レトロスペクティブ(チームでのふりかえり)が時間を書けている割に効果が出ていない感(木曜日)

エネルギーを与えた出来事(幸せになった・安心した)

  • キムチ作り(日曜日)
  • 先輩とペア作業をして学ぶことが多い(Unit test, Git, RxJava)
  • Think Clearlyを読み始めた(水曜日)
  • 大きなタスクを完了にできた(水曜日)
  • e2eによって問題の解決方法が誤っていることに気づけた(金曜日)
  • SATソルバーで数独を解けた(金曜日)

戸惑った出来事や疑問に思った出来事

特になし

話したいこと

  1. SATソルバーで数独を解けた(金曜日)

SATソルバーで数独を解く

最近SATについて理解する必要があり、勉強のために数独を解かせてみました。SATは充足可能性問題(Satisfiability problem)のことで、たくさんの論理式を与えて、それらの論理式がすべて真となるような変数を探すという問題です。

具体例を示す前に説明に必要な用語があるので説明します。

  • リテラル:真か偽を示す変数
  • 節(Clause):リテラルをORでつないだもの
  • 連言標準形(CNF):節をANDでつないだもの

具体的には以下のような問題があったとします。

以下の条件を満たすx, y, zを求めよ

  1. xまたはyが真である
  2. xが偽である又はzが真である
  3. yは偽である

この時x, y, zがリテラル、xまたはyが真であるが節、1,2,3の条件を全部で連言標準形のことを指しています。この問題をSATソルバーを使って解くとすると以下のようなコードで解くことができます。

from pysat.solver import Minisat22

x=1
y=2
z=3

solver = Minisat22()

clause1 = [x, y]    #  x or y   = xまたはyが真である
clause2 = [-x, z]   # !x or z   = xが偽である又はzが真である
clause3 = [-y]      # !y        = yは偽である

solver.add_clause(clause1)
solver.add_clause(clause2)
solver.add_clause(clause3)

solver.solve()
solver.get_model()
# -> [1, -2, 3]

最後に出てきた[1, -2, 3]はxが真、yが偽、zが真を表しています。 実際にこの答えで与えられた条件をすべて満たしています。

SATでは上記のように条件を節に置き換えることができれば問題を解くことができます。 この要領で数独も解くことができるらしかったので、実際にプログラムを書いて解いてみました。

9×9の数独の条件としては以下のようなものがあります。

  1. 各マスには1~9のいずれかが入る
  2. 各行に少なくとも1回以上1~9が入る
  3. 各列に少なくとも1回以上1~9が入る
  4. 各ブロック(3×3の区域)に少なくとも1回以上1~9が入る
  5. 各マスに異なる数字が同時に入らない
  6. 各行に同じ数字が入らない
  7. 各列に同じ数字が現れない
  8. 各ブロックに同じ数字が現れない
  9. すでに埋まっている値はそのままである

これらをすべて節として表現し、SATソルバーに与えてあげれば数独が解けるはず。 それでは以下のような問題を考えましょう。

-,-,-,-,-,-,-,7,-
1,-,5,-,3,6,4,-,9
-,7,4,9,-,-,5,-,-
-,-,-,-,-,5,8,-,-
-,1,-,3,-,-,-,-,5
7,-,-,-,-,8,1,-,-
6,4,-,-,-,-,-,-,7
-,3,-,6,2,-,-,8,4
-,-,-,5,9,-,-,-,3

まずは各マスに1~9が入るかどうかという変数が必要なので考えます。 9×9の数独で、各マスに1~9が入るので9×9×9個のリテラルが必要です。 e.g. 一番左上でのマスに1が入るかどうか、一番左上でのマスに2が入るかどうか...

具体的には各マスにユニークな数字を割り当ててあげました。

class LiteralGenerator:
    def __init__(self):
        self.idx = 0
    
    def next(self):
        self.idx += 1
        return self.idx

gen = LiteralGenerator()
net = []
for i in range(9):
    matrix = []
    for j in range(9):
        row = [gen.next() for k in range(9)]
        matrix.append(row)
    net.append(matrix)
# net[行][列][数値]

一番上の行の7はnet[0][7][6]で70ということになります。 (ここを理解するのに苦労しました。)

それではここから一つ一つの条件を考えていきます。

1. 各マスには1~9のいずれかが入る

例えば左上のマスに1~9のいずれかが入ることを表現したければ、

net[0][0][0] or net[0][0][1] or ... or net[0][0][8]

で表現できます。これを全マス分の節を作る必要があります。

cnf = CNF()

for row in range(9):
    for col in range(9):
        cnf.append([net[row][col][num] for num in range(9)])

2. 各行に少なくとも1回以上1~9が入る

例えば1行目に少なくとも1が1回以上入ることを表現したければ、

net[0][0][0] or net[0][1][0] or ... or net[0][8][0]

で表現できます。これを全行、全数字分の節を作る必要があります。

for num in range(9):
    for row in range(9):
        cnf.append([net[row][col][num] for col in range(9)])

3. 各列に少なくとも1回以上1~9が入る

例えば1列目に少なくとも1が1回以上入ることを表現したければ、

net[0][0][0] or net[1][0][0] or ... net[8][0][0]

で表現できます。これを全列、全数字分の節を作る必要があります。

for num in range(9):
    for col in range(9):
        cnf.append([net[row][j][num] for row in range(9)])        

4. 各ブロック(3×3の区域)に少なくとも1回以上1~9が入る

例えば左上のブロックに関して少なくとも1が1回以上入ることを表現したければ、

net[0][0][0] or ... or net[1][1][0] or net[2][2][0]

で表現できます。これを全ブロック、全数字分の節を作る必要があります。 (この条件は実装するのが結構迷った)

for num in range(9):
        for j in range(9):
            cnf.append([net[(j//3)*3+(k//3)][j%3*3+k%3][num] for k in range(9)])

# 行は0, 1, 2 × 3, 3, 4, 5 × 3, ...と変化する必要がある
# 列は0, 0, 0, 1, 1, 1, 2, 2, 2, ...と変化する必要がある

5. 各マスに異なる数字が同時に入らない

左上のマスに1と2が同時に入らないこと表現したければ、

-net[0][0][0] or -net[0][0][1]

で表現できます。ちょっと分かりづらいですが、net[0][0][0] and net[0][0][1]の否定を表したいのでド・モルガンの法則を用いてorになおすと上記のようになります。 これを全マス分の節を作る必要があります。

for row in range(9):
    for col in range(9):
        for num1 in range(9):
            for num2 in range(num1+1, 9):
                cnf.append([-net[row][col][num1], -net[row][col][num2])

6. 各行に同じ数字が入らない

1行目の一番左とその右のマスに1が複数回現れないことを表現したければ、

-net[0][0][0] or -net[0][1][0]

で表現できます。全行、全数字分の節を作る必要があります。

for num in range(9):
    for row in range(9):
        for col1 in range(9):
            for col2 in range(col1+1, 9):
                cnf.append([-net[row][col1][num], -net[row][col2][num])

7. 各列に同じ数字が現れない

1列目に一番上とその下のマスに1が複数回現れないことを表現したければ、

-net[0][0][0] or -net[1][0][0]

で表現できます。全列、全数字分の節を作る必要があります。

for num in range(9):
    for col in range(9):
        for row1 in range(9):
            for row2 in range(row1+1, 9):
                cnf.append([-net[row1][col][num], -net[row2][col][num])

8. 各ブロックに同じ数字が現れない

左上のブロックの左上とその右に1が複数回現れないことを表現したければ、

-net[0][0][0] or -net[0][1][0]

で表現できます。全ブロック、全数字分の節を作る必要があります。

for i in range(9):
    for j in range(9):
        for k in range(j+1, 9):
            row1 = (i//3)*3+j//3
            row2 = (i//3)*3+k//3
            col1 = i%3*3+j%3
            col2 = i%3*3+k%3
            cnf.append([-net[row1][col1][0], -net[row2][col2][0]])

9. すでに埋まっている値はそのままである

今回与えられた問題は以下のようなものなので、数字が入っている部分に関して節を作っていきます。

-,-,-,-,-,-,-,7,-
1,-,5,-,3,6,4,-,9
-,7,4,9,-,-,5,-,-
-,-,-,-,-,5,8,-,-
-,1,-,3,-,-,-,-,5
7,-,-,-,-,8,1,-,-
6,4,-,-,-,-,-,-,7
-,3,-,6,2,-,-,8,4
-,-,-,5,9,-,-,-,3

右上の7はnet[0][7][6]、1行2列目の1はnet[1][0][0]という感じで表現してきます。 ここの処理は詳しい処理は省略しちゃいます。

全部の節が揃った!

この数独を解くために作成した節はすべてで9426個でリテラルは最初に述べたとおり729個でした。実際に解いてみると、

solver = Minisat22()
solver.append_formula(cnf.clauses, no_return=False)
solver.solve()

ans = np.array(solver.get_model()).reshape(9, 9, 9)
ans = ans[ans > 0].reshape(9, 9)
ans = ans % 9
print(np.where(ans == 0, 9, ans))

->
array([[9, 6, 2, 4, 5, 1, 3, 7, 8],
       [1, 8, 5, 7, 3, 6, 4, 2, 9],
       [3, 7, 4, 9, 8, 2, 5, 6, 1],
       [4, 9, 6, 1, 7, 5, 8, 3, 2],
       [2, 1, 8, 3, 6, 9, 7, 4, 5],
       [7, 5, 3, 2, 4, 8, 1, 9, 6],
       [6, 4, 9, 8, 1, 3, 2, 5, 7],
       [5, 3, 1, 6, 2, 7, 9, 8, 4],
       [8, 2, 7, 5, 9, 4, 6, 1, 3]])

解けた!すごい!

最後に

学んだことをまとめようとするとついつい長くなっちゃいました。最近読んだ本とかの感想や先輩から学んだことも書きたかったけど、書くのが疲れちゃいました笑 週末じゃない時にも書いて投稿しようかなぁ。。。

全然関係ないけど、今週のキムチ作りの時に食べたユッケジャンクッパが美味しかった!

f:id:makky_emmanuel:20210320192709j:plain
ユッケジャンクッパ