English | Japanese CSPSAT
(until FY2011)

About Project

  The progress of SAT technologies has been successful in various domains that require high performance reasoning. In the previous project, CSPSAT, we applied SAT technologies to constraint satisfaction problems (CSPs) and achieved top-class results such as the development of the state-of-the-art CSP solver -- Sugar.
  This project, CSPSAT2, advances the existing SAT-based constraint programming (CP) systems by the following extensions: the adaptation for both real number domain and symbolic domain, soft constraints, and the addition and deletion of constraints. Our goal is then the development of a high performance reasoning engine for intractable and hard problems for existing SAT technologies. It will contribute to the progress of technologies of SAT and CP.

Research Subject (tentative)

A. Extensions for flexible constraints
SAT-encoding of Max-CSP
SAT-encoding of weighted CSP
Incremental solving
B. Extensions for dynamic constraints
Dynamic addition and deletion of constraints
Incremental solving
C. Domain descriptions
Real number domain
Symbolic domain
D. Applications
Mixed-integer programming problem
System verification
Planning problem
Scheduling problem
Systems Biology

Project Members (in no particular order)

Naoyuki Tamura (Principal Investigator)
Information Science Technology Center, Kobe University
Katsumi Inoue (Co-Investigator)
Principles of Informatics Research Division, National Institute of Informatics
Mutsunori Banbara (Co-Investigator)
Information Science Technology Center, Kobe University
Hidetomo Nabeshima (Co-Investigator)
Interdisciplinary Graduate School of Medical and Engineering, University of Yamanashi
Takehide Soh (Co-Investigator)
Information Science Technology Center, Kobe University
Tenda Okimoto (Co-Investigator)
Graduate School of Maritime Sciences, Kobe University
Tomoya Tanjo (Co-Investigator)
Transdisciplinary Research Integration Center, Research Organization of Information and Systems
Laurent Simon (Research Collaborator)
LRI, University Paris 11


The JSPS Grant-in-Aid for Scientific Research (B)
Research Subject
Realization of High-Performance and Flexible Constraint Programming Systems Using Propositional Inference Techniques
Project Number

Tamura Lab.T. Soh
since 24th March 2009