ニュース

最新情報と今後の予定です．

2020

<2020-11-06 Fri>

令和2年度前期全学共通教育ベストティーチャー賞 を受賞しました．

<2020-01-01 Wed>

あけましておめでとうございます． 今年の年賀状 です．

2019

<2019-11-06 Wed>

Best Paper Award at The 6th International Workshop on Smart Wireless Communications (SmartCom 2019)

  • Tomoki Takahashi, Tomio Kamada, Chikara Ohta, Naoyuki Tamura, Taka Maeno: Joint Channel and AP/STA Assignment for Infrastructure-Mode IEEE 802.11 Multi-Interface Wireless Mesh Networks

<2019-11-02 Sat>

Sugar is used in the following very interesting paper.

<2019-06-07 Fri>

人工知能学会 2019年度 全国大会優秀賞 を受賞しました．

<2019-08-28 Wed>

以下の解説論文が，日本ソフトウェア科学会第7回 解説論文賞 を受賞しました．

<2019-01-29 Tue>

高度教養セミナー工学部 (情報知能工学) のスライドです．

<2019-01-01 Tue>

あけましておめでとうございます． 今年の年賀状 です．

2018

<2018-10-07 Sun>

Math Power 2018の世界最大合体ナンプレについて， Copris を用いてギネス記録としての検証を行いました．

<2018-09-18 Tue>

以下の論文が情報処理学会の 特選論文 に選定されました (https://www.ipsj.or.jp/award/ssp_award.html)．

  • 寸田 智也, 宋 剛秀, 番原 睦則, 田村 直之, 井上 克巳

  • SAT技術を用いたペトリネットのデッドロック検出手法の提案

  • 情報処理学会論文誌, Vol.59, No.9, pp.1749-1760 (2018-09-15)

  • http://id.nii.ac.jp/1001/00191384/

<2018-08-28 Tue>

Takehide Soh's sCOP won in two categories (sequential CSP and parallel CSP) at an international CSP solver competition (XCSP18).

<2018-05-21 Mon>

Knuth先生の『TAOCP 7.2.2.2 Satisfiability』を読む のページを作成中です．

<2018-02-15 Thu>

情報処理学会会誌 2018年3月号の小特集「LSIの配線問題—DAシンポジウムの配線問題解法コンテスト」で， 以下の記事が掲載されました．

<2018-01-04 Thu>

あけましておめでとうございます． 今年の年賀状 です．

2017

<2017-03-01 Wed>

田村研究室M2の迫龍哉さんが，2016年度人工知能学会全国大会での発表に関して 全国大会優秀賞 を受賞しました．

<2017-01-04 Wed>

あけましておめでとうございます． 今年の年賀状 です．

2016

<2016-11-15 Tue>

10th CSPSAT Seminar を神戸大学で開催しました． 講演者および参加者の皆様ありがとうございました．

<2016-09-08 Thu>

日本ソフトウェア科学会 第20回 研究論文賞 を受賞しました． 本論文賞の選定は，日本ソフトウェア科学会研究論文賞表彰規定に基づき， 2014年発行の「コンピュータソフトウェア」に掲載された全ての研究論文を対象として， 厳正な審査のもとに行われたものです． 筆頭著者の則武さんは田村研究室OBです．

  • 則武治樹, 番原睦則, 宋剛秀, 田村直之, 井上克巳: パッキング配列問題の制約モデリングとSAT符号化， コンピュータソフトウェア，Vol.31, No.1, p.116-130, 2014. (J-Stage)

<2016-07-15 Fri>

情報処理学会会誌 「情報処理」2016年8月号 で 「SAT技術の進化と応用 〜パズルからプログラム検証まで〜」が特集されました．

  1. SAT技術の進化 (番原睦則・鍋島英知)

  2. SATとパズル─問題をいかにSATソルバーで解くか─ (田村直之・宋　剛秀・番原睦則)

  3. SATとラムゼー数〜数学の未解決問題への挑戦〜 (藤田　博・越村三幸)

  4. SATとAI (井上克巳)

  5. SATソルバーの最近の進展 (鍋島英知・岩沼宏治・井上克巳)

  6. MaxSAT：SATの最適化問題への拡張─MaxSATソルバーの活用法─ (越村三幸・藤田　博)

  7. SMTソルバーによるプログラム検証 (石井大輔・上田和紀)

<2016-01-09 Sat>

Donald Knuth's new book is arrived! Our works are refereed in pages 100, 171, 264, 267, and 268. The order encoding is explained in pages 98–101, 114, 120, 170–173, 190, 268, and 281.

2015

<2015-12-19 Sat>

父の著書が出版されました．

<2015-12-11 Fri>

We released the following softwares.

<2015-09-24 Thu>

Donald Knuth 先生から 小切手 が届きました．うれしい!

<2015-09-24 Thu>

田村研究室M1の川原征大さんが， 日本ソフトウェア科学会第32回大会での発表に関して 学生奨励賞 を受賞しました．

<2015-08-26 Wed>

情報処理学会 システムとLSIの設計技術研究会より， 優秀論文賞 を受賞しました．

<2015-08-27 Thu>

iSugar+GlueMiniSat チーム (メンバー: 迫龍哉, 川原征大, 田村, 番原, 宋, 鍋島)は， 2015年8月27日に開催された DAシンポジウム2015 アルゴリズムデザインコンテスト において第1位となり 最優秀賞 を受賞しました．

<2015-07-21 Tue>

田村研究室M2の兼行大将さんが， 第29回 人工知能学会全国大会での発表に関して 全国大会優秀賞 を受賞しました．

<2015-07-14 Tue>

講義資料として Knuth先生の『TAOCP 7.2.2.2 Satisfiability』を読む を作成中です． 26ページ「SAT examples—summary」までが目標ですが，当分かかりそうです…

<2015-07-12 Sun>

近畿和算ゼミナールで 「 素数ものさしの考察 」を発表しました．

<2015-01-24 Sat>

パズルーム のページを公開しました．

2014

<2014-12-25 Thu>

小柳義夫著「 HPCの歩み50年 」(HPCwire Japan) で， Lispマシン と Prologマシン が紹介されました．

<2014-12-19 Fri>

日経テクノロジーオンラインの記事 IC配線設計に通じるパズルの「ナンバーリンク」、自動で解くアルゴリズムでコンテスト開催 (富士通研究所 富田憲範氏 執筆)の中で， Sugar, GlueMiniSat, Copris が紹介されました (「全問正解の神戸大学と山梨大学のチームが最優秀賞」のページ)． Sugar+GlueMiniSat チーム (メンバー: 田村, 番原, 宋, 鍋島)は，2014年8月28日に開催された DAシンポジウム アルゴリズムデザインコンテスト において全問正解で第1位となり 最優秀賞 を受賞しました．

<2014-12-14 Sun>

研究集会 実験計画法および関連する組合せ構造2014 で特別講演を行いました．

<2014-12-10 Wed>

宋剛秀先生 が，日本ソフトウェア科学会 第31回大会 高橋奨励賞 (2014)を受賞されました．

<2014-02-16 Sun>

田村三郎 (神戸大学名誉教授，数学者)について のページを作成しました．

2013

<2013-12-12 Thu>

Recently, I found a web page http://www.luschny.de/math/rulers/PrimeRulers.html by Peter Luschny in which he mentioned to my article "Complete List of Prime Number Rulers". Prime number ruler of length 18 is originally invented by the Institute of Fuben-eki System (organized by Hiroshi Kawakami of Kyoto University). A sequence of possible lengths of minimal prime number rulers is registered as A227956 of the On-Line Encyclopedia of Integer Sequences.

<2013-07-24 Wed>

ERATO湊離散構造処理系プロジェクト との共催で 論理と推論の理論, 実装, 応用に関する合同セミナー を開催しました．

<2013-07-12 Fri>

GlueMiniSat solver developmed by Hidetomo Nabeshima (Yamanashi University) won the silver medal in "Sequential, Application, Certified UNSAT" track at SAT Competition 2013. Hidetomo Nabeshima is a core member of CSPSAT project.

<2013-07-12 Fri>

QMaxSAT solver by Miyuki Koshimura (Hasegawa Laboratory, Kyushu University) won the silver medal in Partial Max-SAT Industrial category at Eighth Max-SAT Evaluation. Miyuki Koshimura was a core memeber of CSPSAT project.

<2013-03-17 Sun>

九州大学 長谷川研究室 藤田先生がSAT技術を用いて， ラムゼー数 R(4,8) の下界を58に更新しました (http://opal.inf.kyushu-u.ac.jp/~fujita/ramsey.html)． 藤田先生は CSPSAT プロジェクトの中心メンバーです．

<2013-02-01 Fri>

Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems を公開しました．

<2013-01-29 Tue>

PBSugar: A SAT-based Pseudo-Boolean Solver を公開しました．

2012

<2012-10-18 Thu>

KAISER2010導入チームが 学長表彰「特別賞」 を受賞しました．

<2012-06-18 Mon>

九州大学 長谷川研究室 越村先生開発の QMaxSAT solver が Seventh Max-SAT Evaluation の Partial Max-SAT Industrial and Crafted category で優勝しました． 越村先生は CSPSAT プロジェクトの中心メンバーです．

<2012-06-18 Mon>

本條さんと丹生さん開発の ShinMaxSat solver が Seventh Max-SAT Evaluation の Partial Weighted Max-SAT Crafted category で2位になりました． 本條さんと丹生さんは，我々の研究室のメンバーです．

<2012-04-16 Mon>

神戸大学Lispマシン が情報処理学会の情報処理技術遺産に認定され， システム情報学研究科棟の玄関ホールに展示されています． これを機会に 神戸大学工学部システム工学科第4講座で開発された計算機 のページを作成しました．

2011

<2011-11-20 Sun>

前川禎男先生 叙勲祝賀会および前川研究室 研究交流会 を開催しました．

<2011-08-05 Fri>

Prolog Cafe が開発ツール Gerrit で利用されています (Release notes for Gerrit 2.2.2). Gerrit はWebベースのコードレビューシステムで， Android 等の開発に利用されています．

<2011-07-01 Fri>

山梨大学 鍋島研究室 の鍋島先生開発の GlueMiniSat solver が SAT competition 2011 の UNSAT Application category で優勝， SAT+UNSAT Application cateogry および multicore track の UNSAT Application category で2位になりました． 鍋島先生は CSPSAT プロジェクトの中心メンバーです．

<2011-07-01 Fri>

九州大学 長谷川研究室 越村先生開発の QMaxSAT solver が Sixth Max-SAT Evaluation の Partial Max-SAT Industrial category で優勝， Crafted category で2位になりました． 越村先生は CSPSAT プロジェクトの中心メンバーです．

<2011-01-31 Mon>

人工知能学会 第81回 人工知能基本問題研究会 (SIG-FPAI) (2011年1月31日–2月1日, 山梨大学)で Sugar について招待講演を行いました(発表スライド)．

2010

<2010-07-16 Fri>

九州大学 長谷川研究室 越村先生開発の QMaxSAT solver が Fifth Max-SAT Evaluation の Partial Max-SAT Industrial category で優勝， Crafted category で2位になりました． 越村先生は CSPSAT プロジェクトの中心メンバーです．

<2010-07-15 Thu>

CICLOPS-WLPE 2010 で Sugar について招待講演を行いました(発表スライド)．

<2010-04-19 Mon>

FLOPS 2010 で Sugar について招待講演を行いました(発表スライド)．

<2010-01-01 Fri>

CSPSAT プロジェクトのメンバーで 特集：「最近のSAT技術の発展」を 人工知能学会 学会誌に分担執筆しました (特集「最近のSAT技術の発展」にあたって)．

2009

<2009-10-02 Fri>

第4回国際制約ソルバー競技会 で， 本研究室で開発しているソフトウェアである Sugar が， 全7部門中の 3部門で優勝 しました． 本年度の競技会には各国から9チーム14ソルバーが参加し， SugarはAlldiff, Alldiff+Elt+Wsum, Alldiff+Cumul+Elt+Wsumの3部門で第1位となりました． これらは前回のGLOBAL部門が3つに分かれたものです． 詳しい結果は こちら をご覧ください． なおMax-CSP Solver Competitionは，参加ソルバーがSugarのみだったため 残念ながら開催されませんでした．

2008

<2008-09-14 Sun>

第3回国際制約ソルバー競技会 で， 本研究室で開発しているソフトウェアである Sugar が， CSP Solverの5部門およびMax-CSP Solverの5部門の全10部門中， 4部門で優勝 しました． このCompetitionは， スケジューリング問題や長方形パッキング問題等， 解くのが非常に難しい制約充足問題(CSP)を対象として， 解を探索するプログラムの性能を競うものです． 本年度のCSP Solver Competition (全5部門)には 各国から14チーム，24ソルバーが参加し， SugarはGLOBAL部門で第1位となりました． Max-CSP Solver Competition (全5部門)には 4チーム，8ソルバーが参加し， Sugarは2-ARY-INT, N-ARY-INT, GLOBALの3部門で第1位となりました． 詳しい結果は こちら をご覧ください．