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

Research and Development on Constraint Answer Set Programming Using SAT Encoding

Research Project

Project/Area Number 15K00099
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Software
Research InstitutionKobe University

Principal Investigator

BANBARA Mutsunori  神戸大学, 情報基盤センター, 准教授 (80290774)

Co-Investigator(Kenkyū-buntansha) 田村 直之  神戸大学, 情報基盤センター, 教授 (60207248)
宋 剛秀  神戸大学, 情報基盤センター, 助教 (00625121)
Co-Investigator(Renkei-kenkyūsha) INOUE Katsumi  国立情報学研究所, 情報学プリンシプル研究系, 教授 (10252321)
Project Period (FY) 2015-04-01 – 2018-03-31
Project Status Completed (Fiscal Year 2017)
Budget Amount *help
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2017: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2016: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2015: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
Keywords解集合プログラミング / 制約プログラミング / SAT技術 / SAT
Outline of Final Research Achievements

We focused research and development on Constraint Answer Set Programming (CASP), an integration of Answer Set Programming (ASP) and Constraint Programming (CP). CASP allows for direct representation of Constraint Satisfaction Problems (CSPs) over finite domains of Integers. We have developed two CASP solvers. One is based on a translation-based approach where a CSP is fully translated into ASP and then solved by an ASP solver. Another is based on a lazy approach where an ASP solver is augmented with dedicated propagators for CSPs. We established the competitiveness of our approach by empirically contrasting our solvers and other different CASP/CP solvers.

Report

(4 results)
  • 2017 Annual Research Report   Final Research Report ( PDF )
  • 2016 Research-status Report
  • 2015 Research-status Report
  • Research Products

    (53 results)

All 2018 2017 2016 2015 Other

All Int'l Joint Research (7 results) Journal Article (18 results) (of which Int'l Joint Research: 11 results,  Peer Reviewed: 17 results,  Open Access: 8 results,  Acknowledgement Compliant: 2 results) Presentation (28 results) (of which Invited: 3 results)

  • [Int'l Joint Research] ポツダム大学(ドイツ)

    • Related Report
      2017 Annual Research Report
  • [Int'l Joint Research] アルトワ大学(フランス)

    • Related Report
      2017 Annual Research Report
  • [Int'l Joint Research] ポツダム大学(ドイツ)

    • Related Report
      2016 Research-status Report
  • [Int'l Joint Research] University of Potsdam(ドイツ)

    • Related Report
      2015 Research-status Report
  • [Int'l Joint Research] Aalto University(フィンランド)

    • Related Report
      2015 Research-status Report
  • [Int'l Joint Research] University of Ferrara(イタリア)

    • Related Report
      2015 Research-status Report
  • [Int'l Joint Research] INRIA Rennes(フランス)

    • Related Report
      2015 Research-status Report
  • [Journal Article] teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming2018

    • Author(s)
      Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
    • Journal Title

      Annals of Operations Research

      Volume: - Issue: 1 Pages: 3-37

    • DOI

      10.1007/s10479-018-2757-7

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Clingcon: The Next Generation2017

    • Author(s)
      Mutsunori Banbara, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub
    • Journal Title

      Theory and Practice of Logic Programming

      Volume: 17(4) Issue: 4 Pages: 408-461

    • DOI

      10.1017/s1471068417000138

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Proposal and Evaluation of Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings2017

    • Author(s)
      Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
    • Journal Title

      International Journal on Artificial Intelligence Tools

      Volume: 26(1) Issue: 01 Pages: 1760005-1760005

    • DOI

      10.1142/s0218213017600053

    • Related Report
      2017 Annual Research Report 2016 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Solving Multiobjective Discrete Optimization Problems with Propositional Minimal Model Generation2017

    • Author(s)
      Takehide Soh, Mutsunori Banbara, Naoyuki Tamura, Daniel Le Berre
    • Journal Title

      Proceedings of the 23rd International Conference on Principles and Practice of Constraint Programming (CP 2017)

      Volume: 10416 Pages: 596-614

    • DOI

      10.1007/978-3-319-66158-2_38

    • ISBN
      9783319661575, 9783319661582
    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] catnap: Generating Test Suites of Constrained Combinatorial Testing with Answer Set Programming2017

    • Author(s)
      Mutsunori Banbara, Katsumi Inoue, Hiromasa Kaneyuki, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura
    • Journal Title

      Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2017)

      Volume: 10377 Pages: 265-278

    • DOI

      10.1007/978-3-319-61660-5_24

    • ISBN
      9783319616599, 9783319616605
    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] 解集合プログラミングによるカリキュラムベース・コース時間割編成2017

    • Author(s)
      番原睦則, 井上克巳, ベンジャミン カウフマン, トルステン シャウブ, 宋剛秀, 田村直之, フィリップ ワンコ
    • Journal Title

      第29回RAMPシンポジウム論文集

      Volume: - Pages: 73-88

    • Related Report
      2017 Annual Research Report
    • Int'l Joint Research
  • [Journal Article] SAT-based Constraint Programming Systems and Related Technologies2017

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

      Computer Software

      Volume: 34 Issue: 1 Pages: 1_67-1_80

    • DOI

      10.11309/jssst.34.1_67

    • NAID

      130006855237

    • ISSN
      0289-6540
    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Modeling Delayed Dynamics in Biological Regulatory Networks from Time Series Data2017

    • Author(s)
      Emna Ben Abdallah, Tony Ribeiro, Morgan Magnin, Olivier H. Roux, Katsumi Inoue
    • Journal Title

      Algorithms

      Volume: 10(1) Issue: 1 Pages: 8-8

    • DOI

      10.3390/a10010008

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Analyzing resilience properties in oscillatory biological systems using parametric model checking2016

    • Author(s)
      Alexander Andreychenko, Morgan Magnin, Katsumi Inoue
    • Journal Title

      BioSystems

      Volume: 149 Pages: 50-58

    • DOI

      10.1016/j.biosystems.2016.09.002

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] An Incremental SAT Solving Library and its Applications2016

    • Author(s)
      迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
    • Journal Title

      Computer Software

      Volume: 33 Issue: 4 Pages: 4_16-4_29

    • DOI

      10.11309/jssst.33.4_16

    • NAID

      130005290581

    • ISSN
      0289-6540
    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] SAT技術の進化2016

    • Author(s)
      番原睦則, 鍋島英知
    • Journal Title

      情報処理

      Volume: 57(8) Pages: 704-709

    • Related Report
      2016 Research-status Report
    • Peer Reviewed
  • [Journal Article] SATとパズル2016

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

      情報処理

      Volume: 57(8) Pages: 710-715

    • Related Report
      2016 Research-status Report
    • Peer Reviewed
  • [Journal Article] Implementing Efficient All Solutions SAT Solvers2016

    • Author(s)
      Takahisa Toda, Takehide Soh
    • Journal Title

      Journal of Experimental Algorithmics

      Volume: 21(1) Pages: 1-44

    • DOI

      10.1145/2975585

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming2016

    • Author(s)
      Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Torsten Schaub, Takehide Soh, Naoyuki Tamura, and Philipp Wanko
    • Journal Title

      Proceedings of the 11th International Conference on the Practice and Theory of Automated Timetabling (PATAT 2016)

      Volume: - Pages: 13-32

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] \sum_x-Optimal Solutions in Highly Symmetric Multi-Objective Timetabling Problems2016

    • Author(s)
      Maxime Clement, Tenda Okimoto, Katsumi Inoue, and Mutsunori Banbara
    • Journal Title

      Proceedings of the 11th International Conference on the Practice and Theory of Automated Timetabling (PATAT 2016)

      Volume: - Pages: 63-79

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] Inference of Delayed Biological Regulatory Networks from Time Series Data2016

    • Author(s)
      Emna Ben Abdallah, Tony Ribeiro, Morgan Magnin, Olivier F. Roux, Katsumi Inoue
    • Journal Title

      Proc. 14th Int'l Conf. on Computational Methods in Systems Biology (CMSB 2016), Lecture Notes in Bioinformatics

      Volume: 9859 Pages: 30-48

    • DOI

      10.1007/978-3-319-45177-0_3

    • ISBN
      9783319451763, 9783319451770
    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings2015

    • Author(s)
      Takehide Soh, Mutsunori Banbara, and Naoyuki Tamura
    • Journal Title

      Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015, SAT and CSP track)

      Volume: - Pages: 421-428

    • DOI

      10.1109/ictai.2015.70

    • NAID

      40020657481

    • Related Report
      2015 Research-status Report
    • Peer Reviewed
  • [Journal Article] aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming2015

    • Author(s)
      Mutsunori Banbara, Martin Gebser, Katsumi Inoue, Max Ostrowski, Andrea Peano, Torsten Schaub, Takehide Soh, Naoyuki Tamura, and Matthias Weise
    • Journal Title

      Proceedings of the 13th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR 2015)

      Volume: LNAI9345 Pages: 112-126

    • DOI

      10.1007/978-3-319-23264-5_10

    • ISBN
      9783319232638, 9783319232645
    • Related Report
      2015 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] SAT ソルバーの進歩2017

    • Author(s)
      番原睦則
    • Organizer
      2017年電子情報通信学会総合大会
    • Place of Presentation
      名城大学 (愛知県・名古屋市)
    • Year and Date
      2017-03-22
    • Related Report
      2016 Research-status Report
    • Invited
  • [Presentation] ブール基数制約を経由した擬似ブール制約のSAT符号化法2017

    • Author(s)
      南雄之, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      人工知能基本問題研究会(第103回)
    • Place of Presentation
      湯布院公民館 (大分県・由布市)
    • Year and Date
      2017-03-13
    • Related Report
      2016 Research-status Report
  • [Presentation] 解集合プログラミングを用いた多層ナンバーリンクの解法2017

    • Author(s)
      坡山直樹, 川原征大, 迫龍哉, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)
    • Place of Presentation
      華やぎの章 慶山 (山梨県・笛吹市)
    • Year and Date
      2017-03-08
    • Related Report
      2016 Research-status Report
  • [Presentation] SugarTracer: SAT型制約ソルバーSugarのトレースツール2017

    • Author(s)
      吉玉元和, 寸田智也, 南雄之, 宋剛秀, 番原睦則, 田村 直之
    • Organizer
      第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)
    • Place of Presentation
      華やぎの章 慶山 (山梨県・笛吹市)
    • Year and Date
      2017-03-08
    • Related Report
      2016 Research-status Report
  • [Presentation] SATソルバーの最新動向と利用技術2017

    • Author(s)
      宋剛秀, 田村直之
    • Organizer
      第19回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)
    • Place of Presentation
      華やぎの章 慶山 (山梨県・笛吹市)
    • Year and Date
      2017-03-08
    • Related Report
      2016 Research-status Report
  • [Presentation] SATソルバーの使い方 ―問題をSATに符号化する方法―2017

    • Author(s)
      田村直之, 宋剛秀, 番原睦則
    • Organizer
      第58回プログラミング・シンポジウム
    • Place of Presentation
      ラフォーレ倶楽部伊東温泉湯の庭(静岡県・伊東市)
    • Year and Date
      2017-01-06
    • Related Report
      2016 Research-status Report
  • [Presentation] Diet-Sugar: ハイブリッドSAT符号化を実装したSAT型制約ソルバー2017

    • Author(s)
      宋剛秀,番原睦則,田村直之
    • Organizer
      第58回プログラミング・シンポジウム
    • Place of Presentation
      ラフォーレ倶楽部伊東温泉湯の庭(静岡県・伊東市)
    • Year and Date
      2017-01-06
    • Related Report
      2016 Research-status Report
  • [Presentation] 解集合プログラミングによるカリキュラムベース・コース時間割編成2017

    • Author(s)
      番原睦則
    • Organizer
      第29回RAMPシンポジウム
    • Related Report
      2017 Annual Research Report
    • Invited
  • [Presentation] SAT から解集合プログラミングへ2017

    • Author(s)
      番原睦則
    • Organizer
      人工知能学会全国大会(第31回) オーガナイズドセッション「OS-2 SAT技術の理論,実装,応用」
    • Related Report
      2017 Annual Research Report
    • Invited
  • [Presentation] ブール基数制約を経由した擬似ブール制約のSAT符号化手法2017

    • Author(s)
      南雄之, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      日本ソフトウェア科学会第34回大会
    • Related Report
      2017 Annual Research Report
  • [Presentation] 解集合プログラミングを用いた3次元ナンバーリンクソルバー2017

    • Author(s)
      坡山直樹, 飯野有軌, 番原睦則, 田村直之
    • Organizer
      DAシンポジウム2017
    • Related Report
      2017 Annual Research Report
  • [Presentation] SAT技術を用いたペトリネットのデッドロック検出手法の提案2017

    • Author(s)
      寸田智也, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      人工知能学会全国大会(第31回)
    • Related Report
      2017 Annual Research Report
  • [Presentation] 制約充足問題のASP符号化に関する一考察2017

    • Author(s)
      坡山直樹, 番原睦則, 宋剛秀, 田村直之
    • Organizer
      人工知能学会全国大会(第31回)
    • Related Report
      2017 Annual Research Report
  • [Presentation] 解集合プログラミングを用いたナンバーリンクの解法に関する一考察2016

    • Author(s)
      坡山直樹, 川原征大, 迫龍哉, 番原睦則
    • Organizer
      DAシンポジウム2016
    • Place of Presentation
      ゆのくに天祥 (石川県・加賀市)
    • Year and Date
      2016-09-14
    • Related Report
      2016 Research-status Report
  • [Presentation] SAT型制約ソルバーを用いた多層ナンバーリンクの解法2016

    • Author(s)
      寸田智也, 南雄之, 吉玉元和, 宋剛秀
    • Organizer
      DAシンポジウム2016
    • Place of Presentation
      ゆのくに天祥 (石川県・加賀市)
    • Year and Date
      2016-09-14
    • Related Report
      2016 Research-status Report
  • [Presentation] SAT技術を用いた正規ペトリネットのデッドロック検出手法の提案2016

    • Author(s)
      寸田智也, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      日本ソフトウェア科学会第33回大会
    • Place of Presentation
      東北大学 (宮城県・仙台市)
    • Year and Date
      2016-09-06
    • Related Report
      2016 Research-status Report
  • [Presentation] SATソルバーを用いた部分グラフ探索のための制約モデル2016

    • Author(s)
      川原征大, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      2016年度 人工知能学会全国大会
    • Place of Presentation
      北九州国際会議場 (福岡県・北九州市)
    • Year and Date
      2016-06-06
    • Related Report
      2016 Research-status Report
  • [Presentation] SAT型制約ソルバーによるナンバーリンクの解法とその評価2016

    • Author(s)
      迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知
    • Organizer
      2016年度 人工知能学会全国大会
    • Place of Presentation
      北九州国際会議場 (福岡県・北九州市)
    • Year and Date
      2016-06-06
    • Related Report
      2016 Research-status Report
  • [Presentation] クラウド上のソフトウェア要素最適配置問題の解法2016

    • Author(s)
      田村直之, 井上克巳, 鍋島英知, 番原睦則, 宋剛秀
    • Organizer
      人工知能基本問題研究会(第100回)
    • Place of Presentation
      熊本市民会館 (熊本県熊本市中央区桜町)
    • Year and Date
      2016-03-27
    • Related Report
      2015 Research-status Report
  • [Presentation] 解集合プログラミングを用いた制約組合せテストケース生成2016

    • Author(s)
      兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳, 沖本天太
    • Organizer
      第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016)
    • Place of Presentation
      ダイヤモンド瀬戸内マリンホテル(岡山県玉野市渋川)
    • Year and Date
      2016-03-07
    • Related Report
      2015 Research-status Report
  • [Presentation] インクリメンタルSAT解法を用いた高速ナンバーリンクソルバー2016

    • Author(s)
      迫龍哉, 川原征大, 宋剛秀, 番原睦則, 田村直之, 鍋島英知
    • Organizer
      第18回プログラミングおよびプログラミング言語ワークショップ (PPL 2016)
    • Place of Presentation
      ダイヤモンド瀬戸内マリンホテル (岡山県玉野市渋川)
    • Year and Date
      2016-03-07
    • Related Report
      2015 Research-status Report
  • [Presentation] SATソルバーを用いた制約プログラミングシステムとその応用2016

    • Author(s)
      宋剛秀
    • Organizer
      第57回プログラミング・シンポジウム
    • Place of Presentation
      ラフォーレ倶楽部伊東温泉湯の庭 (静岡県伊東市猪戸)
    • Year and Date
      2016-01-08
    • Related Report
      2015 Research-status Report
  • [Presentation] \Sigma-Optimal Solutions in Multi-Objective Timetabling2015

    • Author(s)
      Maxime Clement, Tenda Okimoto, Katsumi Inoue, and Mutsunori Banbara
    • Organizer
      合同エージェントワークショップ&シンポジウム2015論文集 (JAWS 2015)
    • Place of Presentation
      山中温泉河鹿荘ロイヤルホテル (石川県加賀市山中温泉河鹿町)
    • Year and Date
      2015-09-30
    • Related Report
      2015 Research-status Report
  • [Presentation] SATソルバーを用いた高速な部分グラフ探索ツールの実装と評価2015

    • Author(s)
      川原征大, 宋剛秀, 番原睦則, 田村直之
    • Organizer
      日本ソフトウェア科学会第32回大会
    • Place of Presentation
      早稲田大学西早稲田キャンパス(東京都新宿区大久保)
    • Year and Date
      2015-09-09
    • Related Report
      2015 Research-status Report
  • [Presentation] iSugar : インクリメンタルSAT解法が利用可能なSAT型制約ソルバー2015

    • Author(s)
      迫龍哉, 宋剛秀, 番原睦則, 田村直之, 鍋島英知, 井上克巳
    • Organizer
      日本ソフトウェア科学会第32回大会
    • Place of Presentation
      早稲田大学西早稲田キャンパス(東京都新宿区大久保)
    • Year and Date
      2015-09-09
    • Related Report
      2015 Research-status Report
  • [Presentation] 順序符号化と対数符号化を融合した制約充足問題のハイブリッド符号化2015

    • Author(s)
      宋剛秀, 番原睦則, 田村直之
    • Organizer
      日本ソフトウェア科学会第32回大会
    • Place of Presentation
      早稲田大学西早稲田キャンパス(東京都新宿区大久保)
    • Year and Date
      2015-09-09
    • Related Report
      2015 Research-status Report
  • [Presentation] SAT型制約ソルバーによるナンバーリンクの求解と解の最適化2015

    • Author(s)
      迫龍哉, 川原征大, 田村直之, 番原睦則, 宋剛秀, 鍋島英知
    • Organizer
      情報処理学会システムとLSIの設計技術研究会
    • Place of Presentation
      山代温泉ゆのくに天祥 (石川県加賀市山代温泉19-49-1)
    • Year and Date
      2015-08-26
    • Related Report
      2015 Research-status Report
  • [Presentation] 組合せテストケース生成問題に対する制約解集合プログラミングの適用2015

    • Author(s)
      兼行大将, 番原睦則, 宋剛秀, 田村直之, 井上克巳
    • Organizer
      2015年度人工知能学会全国大会(第29回)
    • Place of Presentation
      公立はこだて未来大学 (北海道函館市亀田中野町)
    • Year and Date
      2015-05-30
    • Related Report
      2015 Research-status Report

URL: 

Published: 2015-04-16   Modified: 2019-03-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi