
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
Support
- Name
- The JSPS Grant-in-Aid for Scientific Research (B)
- Research Subject
- Realization of High-Performance and Flexible Constraint Programming Systems Using Propositional Inference Techniques
- Year
- 2012-2014
- Project Number
- 24300007
since 24th March 2009