| English | Japanese | CSPSAT (until FY2011) |
|
| News | About Project | Seminars & Meetings |
Publications & Softwares |
Softwares
| Software | Description |
|---|---|
| Sugar | (also see web page) |
| Naoyuki Tamura (Kobe University) | |
| Sugar is a SAT-based constraint solver that can solve CSP, COP and MAX-CSP. It won the 1st prizes on several categories of CSP Solver Competition 2008-2009 for two years in a row. | |
| SugarTracer | (also see web page) |
| Naoyuki Tamura (Kobe University) | |
| SugarTracer is a program which can trace SAT solver's progress when working on a CNF file generated by Sugar. All the events of the SAT solver (assigning a variable, reaching a conflict, learning a clause, etc.) are expressed at the original CSP level. | |
| Copris | (also see web page) |
| Naoyuki Tamura (Kobe Universiry) | |
| Copris is developed as a DSL (Domain-Specific Language) for constraint programming embedded in Scala programming language, which is designed to help Scala programmers to be able to easily solve various kinds of problem (e.g. constraint optimization problems). Copris also provides a high performance constraint solving since an award winning constraint solver Sugar is used as its backend. | |
| GlueMiniSat | (also see web page) |
| Hidetomo Nabeshima (University of Yamanashi) | |
| GlueMiniSat is a systematic solver based on MiniSat. It won the 1st prize on SAT Competition 2011 (Application, UNSAT, CPU Time), also won the second prizes on other two categories. It won the 2nd prize on SAT Competition 2013 (Application, certified UNSAT). | |
| QMaxSAT | (also see web page) |
| Miyuki Koshimura (Kyushu University) | |
| QMaxSAT is a MaxSAT solver based on MiniSat. It got the 1st prize on MaxSAT Evaluation 2010, 2011, 2012 (Partial MaxSAT Industrial). It also got the 2nd prize (Partial MaxSAT Industrial) in 2013. | |
| Scarab | (also see web page) |
| Takehide Soh (Kobe University) | |
| Scarab is a prototyping tool for developing SAT-based systems. It provides a rich constraint modeling language on Scala and enables a programmer to rapidly specify problems and to experiment with different modelings. | |
| Azucar | (also see web page) |
| Tomoya Tanjo (Transdisciplinary Research Integration Center) | |
| Azucar is a SAT-based constraint solver using compact order encoding. |
