2018年7月15日日曜日

SAT competition 結果

http://sat2018.forsyte.tuwien.ac.at/downloads/satcomp18slides.pdf

で結果が出ています。やはり上位は、MapleSAT系で占められており、一昨年の登場以来、確固たる潮流を感じます。mainトラックの1位は、前に紹介したNadelさんです。

2018年7月12日木曜日

プレゼンを更新しました

http://www.nurse-scheduling-software.com/publications/presentation_for_hospitals2018.pdf

この資料を見られてかどうかは、知りませんが問い合わせが急に多くなりました。

嘘は、書いていませんが、未だ、目指すところが出来ていないので心苦しいのです。PythonによるDSL(Domain Specific Language)実装が出来たところで、SEさんに腕を奮って頂けると思いますが、先は長いです。

自分は、パナファコムで、FDDの評価をした後、アルプス電気で、基板設計・FDD設計・LSI屋、高周波を少し勉強した後、退社して、その後は、VerilogHDLのコンパイラを書いていました。

言語実装手法もLex/Yaccの時代から変わってきています。この辺は、オープンソースにしてブログで実装を書いていきたいと思います。

2018年7月11日水曜日

商標登録証が届きました インテリナビ

ベンチマーク20-24は、超難問

どうしても、解けなくて悩んでいます。7種の解法を新しく考案したのですが、20を除いて、撃沈してしまいました。最後に、もう一種、考案したので、そちらを試して駄目だったら、いい加減にまとめに入ろうかと思います。 この一年、色々学ぶことが出来て幸せでした。ほとんどフルタイムで、考えることに没頭できました。大学の先生に聞くと、9割ぐらいは、雑用で取られるようなので、頭の悪さを差っぴいても私の方が有利です。この年になると、忘却との戦いが始まるのですが、それでも、未だ色々アイデアは出てくるものだなあ、と我ながら感心します。

新しく購入した本は、
・The Art Of Computer Programming 4A
・繁野麻衣子先生の数理最適化

です。4Aは、有名なKnuth大先生が何十年にも渡って書かれている著作の一部です。そのためにLatexを作ったというのは、有名な話しらしいです。いくつかの参照した論文で言及されていたので、確かめるために買ったのですが、ちょっと今のところ出番はなさそうです。

CuttingPlaneのアプローチは、日本語の文献がほとんどなく、この本(数理最適化)でも僅かしか記述されていませんでしたが、入門的には、十分役に立ちました。むしろ、組み合わせ最適化という分野に突入するまえに、一番最初に読みべき本でした。麻衣子先生は、おちゃめな先生で教わりたかったです。なぜか、この分野の研究者は、女性が多いのですが、どうしてなんでしょうね。 

2018年6月23日土曜日

引用されています。その2

MaxSAT2018関連で、また引用されています。

https://arxiv.org/pdf/1806.07164.pdf

インド工科大学のSaurabh Joshiさんの論文に引用されています。
これは楽しみですね。RubenMartinsさんも著者に入っています。 
インド工科大学については、こちらが詳しいです。https://diamond.jp/articles/-/91668

コンペティションのキックオフ直後に論文が、沢山出てくるのは、キックオフ前に公開してしまうと、
自分の優位性がなくなってしまう可能性があるためです。言い換えれば、前年の技術よりも優位な技術があるということです。しかしながら、次年度以降、誰でも、また、それを土台にして発展させることが可能です。その意味で、MaxSAT コンペティションは、重要な礎となってきましたし、SAT技術の発展に寄与してきたと思います。Communityのオープンな雰囲気は、文化と言ってもよいかもしれません。まだまだ、来年度以降も新しい可能性があると思います。

2018年6月17日日曜日

引用されています。

インテルのイスラエル ハイファ研究所のNadelさんの最新論文で去年出場したmaxrosterが引用されています。
http://www.cs.tau.ac.il/research/alexander.nadel/sat18_maxsat.pdf

全然関係ないですが、イスラエルのハイファというとCPUのコア2アーキテクチャの源になりますね。ハイファはイスラエルのハイテク産業の一大集約地になっています。

Nadelさんは、SAT SolverのCore Extractionという分野で有名な方です。 CPUに限らず、LSIのデザイン検証では、SAT SOLVERはなくてはならない重要なツールになっています。

光栄の至りです。


2018年6月12日火曜日

看護総会

今日(6月12日)、 マルマンコンピュータさんが出展されている、という情報を得ました。高速ソルバー(エンジン)が搭載されています。

是非、デモをご覧いただけたら、と思います。

実は、私も実物は、見たことはないのですが、院内LAN上、WEBブラウザで動くシステムです。基本的には大規模病院向けです。