| English | Japanese | CSPSAT (until FY2011) |
CSPSAT2 (until FY2014) |
Cloud (until FY2015) |
CSPASP (since FY2015) |
|
| News | Project | Seminar Meeting |
Publication Software |
About Project
The progress of SAT technologies has been successful in various domains that require high performance reasoning. Constraint Programming System based on SAT (SAT-based CP System) is a compiler that encodes (translates) a given problem into instances of SAT over propositional formulas. Such SAT-based CP systems are acknowledged as a key technology of developing SAT-based systems. On the other hand, in the world, researchers are starting to apply SAT technology to problems beyond NP.
In this project, our goal is the realization of new SAT-based CP systems adaptable to such “Beyond NP” problems. We evaluate the proposed systems via the research and development of the following subjects.
Research Subjects (plan)
- Extensions to Temporal Logic.
- Multi-Objective Optimization.
- Parallel Solver.
- Applications.
Project Members (in no particular order)
| Naoyuki Tamura | Principal Investigator | Kobe University |
| Katsumi Inoue | Co-Investigator | National Institute of Informatics |
| Mutsunori Banbara | Co-Investigator | Kobe University |
| Hidetomo Nabeshima | Co-Investigator | University of Yamanashi |
| Takehide Soh | Co-Investigator | Kobe University |
| Daniel Le Berre | Research Collaborator | Artois University, CRIL-CNRS UMR 8188 |
Support
- The JSPS Grant-in-Aid for Scientific Research (B)
- Research Subject: Research and Development of a New Constraint Programming System based on SAT
- Year: FY2016 - FY2018
- Project Number: 16H02803
 |
Tamura Lab.T. Soh |