日時:2014年10月15日(水) 15:00~17:00 (14:45より開場) 会場:山梨大学甲府キャンパス 情報メディア館4階会議室
http://sojo.yamanashi.ac.jp/facilities/facil-kofu/media-4froom/ http://www.yamanashi.ac.jp/modules/footer_menu/index.php?content_id=5
命題論理式の充足可能性判定問題(SAT)は,計算機科学における最も基本的で本質的な組合せ問題である.SAT問題を解くソルバーの性能は近年飛躍的に向上しており,数百万の命題変数からなる大規模な問題が求解可能になってきている.この性能向上をうけて,システム検証やスケジューリング,制約充足問題などの分野においてSATを利用した問題解決手法が幅広く利用されている.本発表では,高速SATソルバーの代表的な要素技術と,並列型SATソルバーの研究動向について紹介する.
我々は、高度な専門的知識を要する性能チューニング作業を支援するために、細粒度性能チューニング事例データベースの構築と、その応用として、プロファイリング結果やソースコードの特徴をキーとした、性能向上が期待されるプログラム最適化の予測に取り組んでいる。 細粒度性能チューニング事例データベースとは、専門家によるチューニング事例において、一連のソースコード書き換え履歴から、適用されたと思しきプログラム最適化を自動的に同定し、ソースコードの抽象構文木やプロファイリングデータとリンクさせて機械的処理が可能な形で蓄積したものである。このデータベースから、性能向上が見られた事例を訓練データとして抽出し機械学習を適用することにより、適切なプログラム最適化を予測するための分類器を生成する。 本発表ではこれらの取り組みについて、その概要を説明する。