• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

A Prolog-Based Parallel Execution System for Multiple SAT Solvers

Research Project

Project/Area Number 19700025
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Software
Research InstitutionKobe University

Principal Investigator

BANBARA Mutsunori  Kobe University, 学術情報基盤センター, 准教授 (80290774)

Project Period (FY) 2007 – 2009
Project Status Completed (Fiscal Year 2009)
Budget Amount *help
¥3,270,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥570,000)
Fiscal Year 2009: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2008: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2007: ¥800,000 (Direct Cost: ¥800,000)
KeywordsProlog / SAT / 制約充足問題 / 論理プログラミング / 並列計算
Research Abstract

We have studied a parallel execution system of multiple SAT solvers on a Java-based logic programming system. To evaluate our approach, we used the test case generation problems of combinatorial testing as benchmarks. In our experiments, we succeeded in proving the optimality of known bounds for three problems.

Report

(4 results)
  • 2009 Annual Research Report   Final Research Report ( PDF )
  • 2008 Annual Research Report
  • 2007 Annual Research Report
  • Research Products

    (30 results)

All 2010 2009 2008 2007 Other

All Journal Article (16 results) (of which Peer Reviewed: 14 results) Presentation (10 results) Remarks (4 results)

  • [Journal Article] 制約最適化問題とSAT符号化2010

    • Author(s)
      田村直之, 丹生智也, 番原睦則
    • Journal Title

      人工知能学会誌 25巻1号

      Pages: 77-85

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] SATによるシステム検証2010

    • Author(s)
      番原睦則, 田村直之
    • Journal Title

      人工知能学会誌 25巻1号

      Pages: 122-129

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] 制約最適化問題とSAT符号化2010

    • Author(s)
      田村直之, 丹生智也, 番原睦則
    • Journal Title

      人工知能学会誌 25・1

      Pages: 77-85

    • Related Report
      2009 Annual Research Report
  • [Journal Article] SATによるシステム検証2010

    • Author(s)
      番原睦則, 田村直之
    • Journal Title

      人工知能学会誌 25・1

      Pages: 122-129

    • Related Report
      2009 Annual Research Report
  • [Journal Article] Compiling Finite Linear CSP into SAT, Constraints2009

    • Author(s)
      N. Tamura, A. Taga, S. Kitagawa, M. Banbara
    • Journal Title

      Vol.14Issue.2

      Pages: 254-272

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] Compiling Finite Linear CSP into SAT2009

    • Author(s)
      N.Tamura, A.Taga, S.Kitagawa, M.Banbara
    • Journal Title

      Constraints 14・2

      Pages: 254-272

    • NAID

      120000944873

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Compiling Finite Linear CSP into SAT2009

    • Author(s)
      Naoyuki Tamura
    • Journal Title

      Constraints Vol. 14 Isste 2

      Pages: 254-272

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] System Description of a SAT-based CSP Solver Sugar2008

    • Author(s)
      N. Tamura, T. Tanjo, M. Banbara
    • Journal Title

      Proceedings of the Third International CSP Solver Competition

      Pages: 71-75

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] Sugar++: A SAT-based MAX-CSP/COP Solver2008

    • Author(s)
      T. Tanjo, N. Tamura, M. Banbara
    • Journal Title

      Proceedings of the Third International CSP Solver Competition

      Pages: 77-82

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] Sugar: A CSP to SAT Translator Based on Order Encoding2008

    • Author(s)
      N. Tamura, M. Banbara
    • Journal Title

      Proceedings of the Second International CSP Solver Competition

      Pages: 65-69

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] A SAT-based Method for Solving the Two-dimensional Strip Packing Problem2008

    • Author(s)
      Takehide Soh
    • Journal Title

      Proceedings of the 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA'08) (web)

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] System Description of a SAT-based CSP Solver Sugar2008

    • Author(s)
      Naoyuki Tamura
    • Journal Title

      Proceedings of the Third International CSP Solver Competition

      Pages: 71-75

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Sugar++ : A SAT-based MAX-CSP/COP Solver2008

    • Author(s)
      Tomoya Tanjo
    • Journal Title

      Proceedings of the Third International CSP Solver Competition

      Pages: 77-82

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Sugar: A CSP to SAT Translator Based on Order Encoding2008

    • Author(s)
      Naoyuki Tamura
    • Journal Title

      Proceedings of the Second International CSP Solver Competition

      Pages: 65-59

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] PrologからJavaへのトランスレータ処理系とその応用2007

    • Author(s)
      番原睦則, 田村直之, 井上克己
    • Journal Title

      コンピュータソフトウェア 24巻3号

      Pages: 75-86

    • NAID

      130004638868

    • Related Report
      2009 Final Research Report
    • Peer Reviewed
  • [Journal Article] PrologからJavaへのトランスレータ処理系とその応用2007

    • Author(s)
      番原 睦則
    • Journal Title

      コンピュータソフトウェア 第24巻・第3号

      Pages: 75-86

    • NAID

      130004638868

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Presentation] PrologからJavaへのトランスレータ処理系の設計と実装2009

    • Author(s)
      丹生智也, 番原睦則, 田村直之
    • Organizer
      第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009)
    • Place of Presentation
      高山グリーンホテル
    • Year and Date
      2009-03-10
    • Related Report
      2009 Final Research Report 2008 Annual Research Report
  • [Presentation] SAT変換に基づく制約ソルバーSugar2009

    • Author(s)
      番原睦則, 丹生智也, 田村直之
    • Organizer
      第11回プログラミングおよびプログラミング言語ワークショップ(PPL2009)
    • Place of Presentation
      高山グリーンホテル
    • Year and Date
      2009-03-10
    • Related Report
      2009 Final Research Report 2008 Annual Research Report
  • [Presentation] 制約充足問題のSAT変換とグラフ彩色問題への応用2009

    • Author(s)
      丹生智也, 田村直之, 番原睦則
    • Organizer
      日本ソフトウェア科学会第26回大会
    • Place of Presentation
      島根大学(島根県)
    • Related Report
      2009 Final Research Report
  • [Presentation] 制約充足問題のSAT変換とクセラフ彩色問題への応用2009

    • Author(s)
      丹生智也, 田村直之, 番原睦則
    • Organizer
      日本ンフトウェア科学会第26回大会
    • Place of Presentation
      島根大学(島根県)
    • Related Report
      2009 Annual Research Report
  • [Presentation] グリッド計算環境上でのショップ・スケジューリング問題のSAT変換による解法2007

    • Author(s)
      多賀 明子
    • Organizer
      スケジューリング・シンポジウム2007講演論文集
    • Place of Presentation
      京都大学
    • Year and Date
      2007-09-29
    • Related Report
      2007 Annual Research Report
  • [Presentation] Prolog Cafe: PrologからJavaへのトランスレータ処理系のデモ2007

    • Author(s)
      丹生 智也
    • Organizer
      日本ソフトウェア科学会第24回大会
    • Place of Presentation
      奈良先端科学技術大学院大学
    • Year and Date
      2007-09-12
    • Related Report
      2007 Annual Research Report
  • [Presentation] ショップ・スケジューリング問題のSAT変換による解法2007

    • Author(s)
      田村直之, 多賀明子, 番原睦則, 宋剛秀, 鍋島英知, 井上克己
    • Organizer
      スケジューリング・シンポジウム
    • Place of Presentation
      京都大学
    • Related Report
      2009 Final Research Report
  • [Presentation] グリッド計算環境上でのショップ・スケジューリング問題のSAT変換による解法2007

    • Author(s)
      多賀明子, 田村直之, 北川哲, 番原睦則, 田村直之
    • Organizer
      スケジューリング・シンポジウム
    • Place of Presentation
      京都大学
    • Related Report
      2009 Final Research Report
  • [Presentation] Sugar:SAT変換による制約解消システムのデモ2007

    • Author(s)
      田島宏史, 多賀明子, 丹生智也, 田村直之, 番原睦則
    • Organizer
      日本ソフトウェア科学会第24回大会
    • Place of Presentation
      奈良先端科学技術大学院大学
    • Related Report
      2009 Final Research Report
  • [Presentation] Prolog Cafe:PrologからJavaへのトランスレータ処理系のデモ2007

    • Author(s)
      丹生智也, 田村直之, 番原睦則
    • Organizer
      日本ソフトウェア科学会第24回大会
    • Place of Presentation
      良先端科学技術大学院大学
    • Related Report
      2009 Final Research Report
  • [Remarks]

    • URL

      http://kaminari.istc.kobe-u.ac.jp/PrologCafe/

    • Related Report
      2009 Final Research Report
  • [Remarks]

    • URL

      http://kaminari.istc.kobe-u.ac.jp/PrologCafe/

    • Related Report
      2009 Annual Research Report
  • [Remarks]

    • URL

      http://kaminari.istc.kobe-u.ac.jp/PrologCafe/

    • Related Report
      2008 Annual Research Report
  • [Remarks]

    • URL

      http://kaminari.istc.kobe-u.ac.jp/PrologCafe/

    • Related Report
      2007 Annual Research Report

URL: 

Published: 2007-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi