山梨大学鍋島研究室

命題論理式の充足可能性判定問題 (SAT) は，理論上も実際上も計算機科学の中心的課題の1つです．SAT 技術は，様々な応用領域における推論の基盤技術として注目を集めています．例えば，スケジューリング問題の未解決問題の求解，インテル社のi7プロセッサの検証，Eclipse のコンポーネント間の依存解析に SAT 技術が使われるなど，産学両方において応用が進んでいます．また，チューリング賞受賞者の Knuth 教授著 "The Art of Computer Programming"の4B巻では，序文には「SAT 問題は，非常に多くの問題を解くためのキーであることから，明らかに "killer app" である」と述べられています.

卒業研究では SAT やその関連技術，応用に関する研究だけでなく，自ら取り組みたいテーマを模索することも歓迎します．また，研究を通してプログラミング能力を鍛えるだけでなく，効率よく研究・開発を進めるため，研究・開発用のツールを積極的に導入・自作してもらっています．それにより実践的な問題解決力の養成を図ることも本研究室の特徴です．

メンバー

教員
- 鍋島英知
学生
- 桂献一郎 (M2)
- 名幸大輔 (M2)
- 中村心 (M1)
- 飛田龍一 (M1)
- 市川束紗 (B4)
- 久保田十矢 (B4)
- 手塚匠 (B4)

修士・卒業研究

2024

修士研究
- 小泉冴起「カードベース暗号のモデル検査による頑健性評価と効率化の研究」
- 菅原孝太「ASP を用いたナーススケジューリング問題における充足不能原因の抽出手法」
- 穴山智也「節交換順序の記録方式に基づく決定的並列SATソルバーの提案と評価」
- 中野良春「決定的並列 SAT ソルバーにおける UNSAT 証明の並列検証」
卒業研究
- 武川あさ美「修正勤務表が生成しやすい看護師勤務表の自動生成手法の検討」
- 中村くるみ「附属病院における看護師勤務表自動生成に向けた制約パラメータ抽出手法の提案」
- 中村心「実行時間推定による決定的並列SAT ソルバーの待ち時間削減手法の検討」
- 飛田龍一「非共有メモリ環境における決定的並列SATソルバーフレームワークの検討」
- 三塚拓真「ASPを用いた附属病院医師勤務表の自動生成手法の検討」

2023

修士研究
- 田光宏章「CSPソルバーを用いた複数画像からなる視覚暗号の構成法」
- 小山貴史「直交ラテン方格とその関連問題のCSPソルバーを用いた解法に関する研究」
- 池田佳貴「線形不等式制約を扱うSAT型CSPソルバーに関する研究」
- 吹上翼「決定的並列SATソルバーの大規模化に向けた遅延節交換法の拡張」
卒業研究
- 高澤怜路「ASP を⽤いた看護師勤務表⽣成への優先度付き巨⼤近傍探索の適⽤」
- 桂献一郎「再現性のある並列 ASP ソルバーの実現に向けた静的同期法の実装」
- 名幸大輔「並列 SAT ソルバーにおける学習節共有戦略の有効性評価」

2022

修士研究
- 久保悠「SATソルバを用いた釣り合い型不完備ブロック計画の構成に関する研究」
卒業研究
- 穴山智也「最新逐次 SAT ソルバーへのマイグレーション機能の導入」
- 小泉冴起「カードベース暗号プロトコルのモデル検査による頑健性の評価」
- 菅原孝太「ASP による看護師勤務表自動生成と附属病院における評価」
- 中野良春「MaxSAT 求解のためのPB・CSPソルバーによる最⼩コストヒッティングセット計算の検討」

2021

修士研究
- 早瀬悠真「圧縮SAT問題の求解手法および制約充足問題への適用」
卒業研究
- 田中綜司「ナーススケジューリング問題のASP符号化の提案とその適用事例」
- 池田佳貴「整数線形 CSP のための効率的伝播アルゴリズムの提案」
- 小山貴史「CSP ソルバーを⽤いた差⾏列に基づく直交ラテン⽅格の⽣成⽅」
- 田光宏章「CSP ソルバーを用いた複数画像からなる視覚復号型秘密分散法の定式化」
- 吹上翼「ヘテロジニアス型決定的並列 SAT ソルバーにおける待ち時間低減手法の検討」

2020

卒業研究
- 石田駿斗「SAT ソルバーを利用した自己相関の小さい系列の探索」
- 久保悠「コワーキングスペースの鉄道網上での配置モデルの検討」
- 塚龍二「SAT ソルバを利用したPaley 行列に基づくロケーティングアレイ生成手法」
- 帯津勇斗「決定的並列SATソルバー構築のための汎用的フレームワークの提案」

2019

卒業研究
- 吉見一樹「比率制約を含む研究室配属問題のCSP符号化手法」
- 早瀬悠真「圧縮したSAT問題を直接解くソルバーの開発」
- 藤崎亮人「決定的並列SATソルバーの待ち時間低減のための準決定的探索手法の提案」

2018

修士研究
- 藤井樹「学生を主体とした研究室配属問題の定式化と解法に関する研究」
卒業研究
- 市澤拓美「SAT ソルバーの動的対称性除去における候補節削減手法の提案」
- 神原和裕「ポートフォリオ型並列 SAT ソルバーにおける適応型探索戦略の提案」
- 中尾陸「学習節簡単化手法に基づくSATソルバーのメタ探索戦略の検討」
- 堀内亮祐「動的対称性除去と動的簡単化を統合したSATソルバーの開発」

2017

修士研究
- 後藤優也「決定的並列 SAT ソルバーの高速化に関する研究」
卒業研究
- 小川祥平「ASPを用いたCS時間割作成手法の高速化」
- 範利「分割統治型 SAT 解法のための並列ソルバーの開発」
- 原田翔規「SATソルバーにおける対称性学習節の削減手法の提案」
- 福田晴喜「リスタート戦略改善のための頻出決定変数パターンのマイニング」

2016

修士研究
- 松上寿支「デバッグ能力強化によるプログラミング初学者向け学習法」
卒業研究
- 宇留賀隆広「大規模並列SATソルバーにおける通信時間の低減手法の提案」
- 藤井樹「同順位を含む研究室配属問題のCSPソルバーによる解法」
- 藤江柊輔「ポートフォリオ型SATソルバーのための分類器の自動構築」

2015

修士研究
- 三神直彬「決定変数除去に基づく SAT ソルバーの高速化手法に関する研究」
卒業研究
- 伊藤靖展「フェアな研究室配属のためのCSP符号化手法」
- 後藤優也「ZDD上での効率的な単位伝搬アルゴリズムの実現」
- 小山博史「SATソルバーのためのコミュニティ構造に基づくヒューリスティクスの提案」
- 長谷部洋弥「SAT問題における鳩ノ巣原理適用手法の提案」
- 秋山洋一郎「ASP による時間割構成法の拡張」

2014

修士研究
- 松田龍平「SATソルバーにおけるヒューリスティクスの半自動獲得に関する研究」
- 杉本拓也「SATソルバーのための動的包摂検査に関する研究」
- 渡辺大樹「SAT変換手法における高レベルモデルと充足不能コアの極小化」
卒業研究
- 松上寿支「プログラム初心者支援を目的としたソースコード検索システムの開発」
- 横前菜々子「SATソルバーにおける学習節の深さに基づいた節管理戦略」

2013

修士研究
- 大橋弘幸「並列SATソルバーにおける協調ポートフォリオ戦略に関する研究」
- 田島史也「Scalaによる研究・学習用SATソルバーの開発」
卒業研究
- 古橋燎「節論理式における単位伝播の並列性改善手法の検討」
- 三神直彬「大規模SAT問題求解のための緩和解法」
- PHAN VAN THANH 「制約充足ソルバーSugar用高速SATソルバー開発」

2012

修士研究
- 寄特勇紀「分割統治法に基づく結論発見手続き SOL タブロー計算法のスケーラビリティ向上に関する研究」
- 村松匠「充足可能性判定器に基づく命題論理の結論列挙の効率化に関する研究」
卒業研究
- 杉本拓也「GlueMiniSatへの動的包摂検出手法の導入」
- 都木雅俊「最良優先探索に基づく結論発見器のプロトタイプ開発」
- 森淳「拡張融合法に基づく次世代SATソルバーの提案」
- 渡辺大樹「GlueMiniSatへの充足不能コア抽出手法の実装」

2011

修士研究
- 金澤潤二「シンメトリーを利用した命題論理の充足可能性問題の効率的解法に関する研究」
- 鈴木健士郎「充足可能性判定器に基づく命題論理の結論発見に関する研究」
卒業研究
- 大橋弘幸「学習節評価尺度LBDに基づく並列SATソルバーの開発」
- 鈴木絢「特徴選択による結論発見器SOLARのポートフォリオ型戦略の改善」
- 田島史也「最新SATソルバーへのリスタートコスト低減戦略の導入」
- 渡辺有洋「演習授業録画配信システムにおけるユーザビリティと動画圧縮効率の改善」

2010

修士研究
- 三澤隆造「擬似ブールソルバによる整数線形制約問題の解法に関する研究」
卒業研究
- 松田龍平「頻出飽和集合を用いた SAT 解法効率化手法の検討」
- 石井祐輔「SAT プランニングにおける数値制約の順序符号化による効率改善」
- 寄特勇紀「SOL タブロー計算法の分割統治法による効率化」
- 村松匠「結論発見システム SOLAR へのポートフォリオ型戦略の導入」

2009

修士研究
- 三澤隆造「Sorters Networkを利用した制約充足ソルバの高速化の検討」
卒業研究
- 倉田真人「KKI演習の自動録画配信ステムの開発」
- 金澤潤二「シンメトリー情報に基づく多分岐探索技術の最新SATソルバへの統合」
- 鈴木健士郎「結論発見システムSOLARの適応的探索戦略による効率改善」

2008

修士研究
- 高見明秀「分散協調型並列SATソルバに関する研究」
卒業研究
- 三澤隆造「制約充足ソルバSugarのための順序制約に基づく専用SATソルバの開発」
- 榛葉祐太「単位節伝搬の並列化によるマルチコア環境用SATソルバの試作」
- 多久和遼「進化論的探索手法を用いた人工知能演習用教材の開発」

2007

卒業研究
- 浅田敏弘「強化学習を用いたロボット演習支援環境の製作」
- 楠剛毅「制約最適化問題のための並列分散SATソルバシステムの構築」
- 西牧一俊「検索隠し味抽出の精度向上と安定化に関する研究」

2006

卒業研究
- 関恭「高速スケジューリングのための専用SATソルバの開発」
- 高見明秀「マルチコア環境のための高速並行SATソルバの開発」
- 長澤香里「専門検索エンジンの半自動合成に対する概念構造を用いた名詞汎化」

アクセス

住所：〒400-8511 山梨県甲府市武田4丁目3番11号
建物： B2号館3F

山梨大学 鍋島研究室

目次