SMT SolverであるZ3でお絵かきロジックソルバを書きました。練習です。 コードはこちら。 罠が何箇所かありました。まず、Z3 python bindingで多次元配列を作る方法がわからなかったので、１次元配列の添字を適当にスキップさせて二次元の図形用変数を作りました。これは自明。 解答を作ったあと、それを表示しようとしてハマりました。結果の配列をprintするとTrueやFalseが正しく出てくるのですが、それをアスキーアートに変えようとすると全てTrueになってしまいます。原因は以下のとおり。 >>> import z3 >>> q = z3.Bool('q') >>> s = z3.Solver() >>> s.add(z3.Not(q)) >>> s.check() sat >>> m = s.model() >>> m [q = False] >>> m.eval(q) False >>> not m.eval(q) False >>> help(m.eval(q)) Help on instance of BoolRef in module z3: class BoolRef(ExprRef) つまりm.eval(q)の返り値はBoolRefであってBoolではなく、FalseなBoolRefはpythonの真偽値としてはTrueを持つのでした。 ちなみに効率ですが、10x10の人手で解けるパズルを解くのに8秒とかかかります。ちょっとつらい。2^100の探索よりは圧倒的に速いですが、そもそも人手で解くことが可能なパズルならばもっと高速で解けて欲しいところです。不適切なツールだったということでFA。 それからz3で一般に困りそうなところ。そういえば数年前のICFPCでも困りました。 シングルプロセス 遅い時に高速化をどうすればいいかわからない。

新しいことを始めようと何か書いてみます。ブログはありますがfc2で、いまさらfc2もないと思うので放棄して新しい物を作ることにしました。 はやりを探してHugoを採用。公式ドキュメントとコミュニティが充実しているので情報を探すのが楽です。Qiita/tags/Hugoとかに日本語の記事もあります。 やったこと インストール hugo serverでブラウザで読めるようになるまでチュートリアルをこなす。 適当な文章(これ)を書く。 テーマをいろいろ変えてみる。 G+リンクを付けてみる。 fontawesomeを更新してG+のアイコンを正しくする。 一部のテキストを適当に更新。 bitbucketチェックイン。 github pagesに突っ込む。 インストール $ brew install hugo Macだったのでこれで終了。LinuxならGolangと go get で終わりだと思います。 チュートリアル とりあえず公式のドキュメントを読めばよいです。quickstartを追いかけました。あとは適当に読めばよいです。Hosting on GitHub Pagesを読んでさくっとアップロードしてしまっても良いですが、私はそれを少し日和りました。 Install some themesの作業だけ地味に時間がかかります。テーマを全部落としてくるので。 テーマ テーマを選んでサイトのデザインを変えられますが、これがなかなか苦労しました。迷います。あと不適切なやつもアリマス。 テーマはHugo Theme Showcaseから探します。チュートリアルに従うとテーマが一通りインストールされているので、 --themes の引数を変えて実際に試すこともできます。 実際に触るとテーマがいろいろとバグってたりして楽しいです。自分で文章をいくつか書いて試すことをおすすめします。私が見つけたのは以下の様な例です。 プログラム片のスタイルが崩れる。 config.yamlに指定する変数名がtypoしているので、説明通りに設定しても動かない。 トップページの概要が崩れる。 github pages に突っ込む。 Hosting on GitHub Pagesに概要があります。しかし、あんまりよい手順に見えなかったので理解したうえで別の手順で行いました。 上までの手順を行いサイト例を手元に作る。public以下は作らなくて良い。 bitbuket.orgかどこかにgit pushする。 github.comに公開用レポジトリをつくる。ここには公開されるデータのみが入ることになる。 ウェブインターフェスを用いて適当なREADME.mdを置く。 ウェブインターフェスを用いてgh-pagesブランチを作る。 あとは以下のコマンドを実行。 $ git remote add gh-gh-pages git@github.com:gusmachine/tracker.git $ git subtree add --prefix=public gh-gh-pages gh-pages --squash git fetch gh-gh-pages gh-pages warning: no common commits remote: Counting objects: 3, done. remote: Total 3 (delta 0), reused 0 (delta 0), pack-reused 0 Unpacking objects: 100% (3/3), done. From github.com:gusmachine/tracker * branch gh-pages -> FETCH_HEAD * [new branch] gh-pages -> gh-gh-pages/gh-pages Added dir 'public' $ ls public README.md $ git subtree pull --prefix=public gh-gh-pages gh-pages --squash From github.com:gusmachine/tracker * branch gh-pages -> FETCH_HEAD Subtree is already at commit b9beee57b9945c67e1f3848d9c06d74d3e806f6d. これで、レポジトリは次のようになります。 bitbucket.orgにはhugoの元データが入る。 public以下はgithub.comの公開用レポジトリをsubtreeとして持つことになる。git subtree pushで更新できる。 あと上のチュートリアルで疑問に思ったこと。canonifyurls: true は独自ドメインの直下に置くことにするならおそらく不要です。username.github.io/project/ 以下に置くなら必要そうですが。 残った項目 もう少し文章を足して見られるようにする。 画像を足す方法をまじめに見る。 hugo/Image path 画像はどこに置くのか、contentとstatic/imgとで争いが起きてます。とりあえずstatic/imgに設置。Google Photosに置くアイデアは、直リンクの生成が面倒で挫折。 タグの使い方を理解。 faviconを足す。 旧ブログから誘導。 月別アーカイブやカレンダーを足す。 Markdownだとサムネイルとクリックして大きい画像みたいな作業が面倒なので何か考える。