English | Japanese CSPSAT
(until FY2011)
(until FY2014)
(until FY2015)
(since FY2015)

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


  • 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
since 24th March 2009