CSPSAT3

English | Japanese CSPSAT
(until FY2011)		 CSPSAT2
(until FY2014)		 Cloud
(until FY2015)		 CSPASP
(since FY2015)
ニュース プロジェクト概要 講演会
＆研究会		 研究成果物
(論文・ソフトウェア等)

ソフトウェア成果物

ソフトウェア名 説明
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 ベースの制約 ソルバーです．
sCOP (web page)
  宋剛秀, Daniel Le Berre, 番原睦則, 田村直之
  sCOP は, SAT型の制約ソルバーです. 2018 XCSP3 Competition の2部門で優勝しました.

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

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

Tamura Lab.T. Soh
since 24th March 2009