Software	Description
Sugar	(web page)
	田村直之 (神戸大学)
	Sugar は， 制約充足問題， 制約最適化問題， 最大制約充足問題を解くことができる SAT ベースの制約ソルバーです． CSP Solver Competition 2008-2009 において，二年連続・複数部門で優 勝しています．
SugarTracer	(web page)
	田村直之 (神戸大学)
	SugarTracerは，Sugar によって出力されたCNFをSATソルバーが解く際の変数割当，矛盾発生，節学習等のイベントをCSPレベルで表示するプログラムです．オープンショップ用の描画機能も利用可能です．
Copris	(web page)
	田村直之 (神戸大学)
	Copris は制約プログラミング用のドメイン特化言語として開発され，Scalaのプログラマが簡潔に制約充足問題(CSP) や制約最適化問題(COP) を記述できることを目的に設計されたものです．バックエンドの制約ソルバーとして Sugar を用いており，制約ソルバーとしても高性能です．
GlueMiniSat	(web page)
	鍋島英知 (山梨大学)
	SAT ソルバーの劇的な性能向上と普及に貢献した代表的なソルバー MiniSat を改良した系統的ソルバーです．SAT Competition 2011 の Application 部門において，逐次型ソルバーとして UNSAT クラスで優勝，SAT+UNSAT クラスで準優勝, 2013年にも Certified UNSAT 部門で準優勝するなど，優秀な成績をおさめています．
Scarab	(web page)
	宋剛秀 (神戸大学)
	Scarab はSAT型システムのための開発ツールです．制約プログラミング用のドメイン特化言語を提供しており Copris と同様のツールですが，SAT符号化モジュールも含めて約500行の Scala 言語で書かれておりコンパクトで拡張容易な点が特長です．
Azucar	(web page)
	丹生智也 (新領域融合研究センター)
	Azucar は，コンパクト順序符号化を用いた SAT ベースの制約 ソルバーです．

特集「最近のSAT技術の発展」
人工知能学会誌 第25巻 第1号 (2010年1月)

本特集は以下の8篇の解説から構成されています． まず，特集「最近のSAT技術の発展」にあたって — http://bach.istc.kobe-u.ac.jp/aisat.html で概要を把握した後に，各論を読んでいただくとより理解が深まります．

1. SATソルバーの基礎， 井上克巳，田村直之， 人工知能学会誌，25巻1号，pp.57-67，2010年 — http://ci.nii.ac.jp/naid/110007504953
2. 高速SATソルバーの原理， 鍋島英知，宋剛秀， 人工知能学会誌，25巻1号，pp.68-76，2010年 — http://ci.nii.ac.jp/naid/110007504954
3. 制約最適化問題とSAT符号化， 田村直之，丹生智也，番原睦則， 人工知能学会誌，25巻1号，pp.77-85，2010年 — http://ci.nii.ac.jp/naid/110007504955
4. SMT：個別理論を取り扱うSAT技術， 岩沼宏治，鍋島英知， 人工知能学会誌，25巻1号，pp.86-95，2010年 — http://ci.nii.ac.jp/naid/110007504956
5. モデル列挙とモデル計数， 長谷川隆三，藤田博，越村三幸， 人工知能学会誌，25巻1号，pp.96-104，2010年 — http://ci.nii.ac.jp/naid/110007504957
6. ＊-SAT: SATの拡張， 平山勝敏，横尾真， 人工知能学会誌，25巻1号，pp.105-113，2010年 — http://ci.nii.ac.jp/naid/110007504958
7. SATによるプランニングとスケジューリング， 鍋島英知， 人工知能学会誌，25巻1号，pp.114-121，2010年 — http://ci.nii.ac.jp/naid/110007504959
8. SATによるシステム検証， 番原睦則，田村直之， 人工知能学会誌，25巻1号，pp.122-129，2010年 — http://ci.nii.ac.jp/naid/110007504960

これまでの研究業績 (〜2011年度)

CSPSAT プロジェクトのページをご覧ください．

---

Tamura Lab.T. Soh

since 24th March 2009