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

A Study on Extending SAT Solvers with Cardinality Constraints and its Applications

Research Project

Project/Area Number 25330085
Research Category

Grant-in-Aid for Scientific Research (C)

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

Principal Investigator

Koshimura Miyuki  九州大学, システム情報科学研究科(研究院, 助教 (30274492)

Co-Investigator(Kenkyū-buntansha) HASEGAWA Ryuzo  九州大学, 大学院システム情報科学研究院, 教授 (20274483)
FUJITA Hiroshi  九州大学, 大学院システム情報科学研究院, 准教授 (70284552)
Chikara Noriaki  徳山工業高等学校, 情報電子工学科, 助手 (50290804)
Project Period (FY) 2013-04-01 – 2016-03-31
Project Status Completed (Fiscal Year 2015)
Budget Amount *help
¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,000)
Fiscal Year 2015: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2014: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2013: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
KeywordsSATソルバー / 基数制約 / SAT符号化 / MaxSAT応用 / MaxSATソルバー / 組合せ最適
Outline of Final Research Achievements

The major results of this study are as follows:
(1) Introduce a method of alternating different strategies into SAT solver in order to enhance its performance. (2) Devise two new SAT encodings Modulo Totalizer and Weighted Totalizer for cardinality constraints and give their space complexity. (3) Present methods for solving the following problems with MaxSAT; (i) inductive logic programming, (ii) coalition structure generation, and (iii) reconstructing AES key schedule images. (4) Introduce a mechanism to utilize unsat core in a MaxSAT solver QMaxSAT.

Report

(4 results)
  • 2015 Annual Research Report   Final Research Report ( PDF )
  • 2014 Research-status Report
  • 2013 Research-status Report
  • Research Products

    (27 results)

All 2016 2015 2014 2013 Other

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

  • [Journal Article] Reconstructing AES Key Schedule Images with SAT and MaxSAT2016

    • Author(s)
      Xiaojuan Liao, Hui Zhang, Miyuki Koshimura
    • Journal Title

      IEICE Transactions on Information and Systems

      Volume: E99.D Issue: 1 Pages: 141-150

    • DOI

      10.1587/transinf.2015EDP7223

    • NAID

      130005116199

    • ISSN
      0916-8532, 1745-1361
    • Related Report
      2015 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] MaxSAT Encoding for MC-Net-Based Coalition Structure Generation Problem with Externalities2014

    • Author(s)
      Xiaojuan Liao, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
    • Journal Title

      IEICE Transactions on Information and Systems

      Volume: E97.D Issue: 7 Pages: 1781-1789

    • DOI

      10.1587/transinf.E97.D.1781

    • NAID

      130004519274

    • ISSN
      0916-8532, 1745-1361
    • Related Report
      2014 Research-status Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Extending MaxSAT to Solve the Coalition Structure Generation Problem with Externalities Based on Agent Relations2014

    • Author(s)
      Xiaojuan Liao, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
    • Journal Title

      IEICE Transactions on Information and Systems

      Volume: E97.D Issue: 7 Pages: 1812-1821

    • DOI

      10.1587/transinf.E97.D.1812

    • NAID

      130004519277

    • ISSN
      0916-8532, 1745-1361
    • Related Report
      2014 Research-status Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] SCSat: A Soft Constraint Guided SAT Solver2013

    • Author(s)
      Hiroshi Fujita, Miyuki Koshimura, Ryuzo Hasegawa
    • Journal Title

      Proc. of SAT 2013

      Volume: なし Pages: 415-421

    • DOI

      10.1007/978-3-642-39071-5_32

    • ISBN
      9783642390708, 9783642390715
    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers2013

    • Author(s)
      Toru Ogawa, YangYang Liu, Ryuzo Hasegawa, Miyuki Koshimura, Hiroshi Fujita
    • Journal Title

      Proc. of ICTAI 2013

      Volume: なし Pages: 9-17

    • DOI

      10.1109/ictai.2013.13

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] Using MaxSAT to Correct Errors in AES Key Schedule Images2013

    • Author(s)
      Xiaojuan Liao, Hui Zhang, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
    • Journal Title

      Proc. of ICTAI 2013

      Volume: なし Pages: 284-291

    • DOI

      10.1109/ictai.2013.51

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] Modulo 計算に基づく基数制約のCNF符号化方式の提案と評価2013

    • Author(s)
      小川 徹,劉 洋洋,長谷川 隆三,越村 三幸,藤田 博
    • Journal Title

      九州大学 システム情報科学紀要

      Volume: 18(2) Pages: 85-92

    • NAID

      120005306729

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Presentation] MaxSATを利用したAES暗号鍵の復元法の改良2016

    • Author(s)
      越村三幸,廖暁鵑
    • Organizer
      NII共同研究プロジェクト: クラウド上のソフトウェア最適配置問題の解法 & 解集合プログラミングによるシステム検証 合同ミーティング
    • Place of Presentation
      熊本市民会館
    • Year and Date
      2016-03-28
    • Related Report
      2015 Annual Research Report
  • [Presentation] Modulo計算に基づく重み付MaxSAT問題の基数制約符号化手法の改良2016

    • Author(s)
      有村寿高,長谷川隆三,藤田博,越村三幸,ZHA AOLONG,上村直輝
    • Organizer
      人工知能学会 第100回人工知能基本問題研究会(SIG-FPAI)
    • Place of Presentation
      熊本市民会館
    • Year and Date
      2016-03-27
    • Related Report
      2015 Annual Research Report
  • [Presentation] Introducing Pure Literal Elimination into CDCL Algorithm2016

    • Author(s)
      Aolong Zha, Miyuki Koshimura, Hiroshi Fujita
    • Organizer
      人工知能学会 第99回人工知能基本問題研究会(SIG-FPAI)
    • Place of Presentation
      湯の原ホテル(仙台市)
    • Year and Date
      2016-01-21
    • Related Report
      2015 Annual Research Report
  • [Presentation] Inductive Logic Programming Using a MaxSAT Solver2015

    • Author(s)
      Noriaki Chikara, Miyuki Koshimura, Hiroshi Fujita, Ryuzo Hasegawa
    • Organizer
      5th International Conference on Inductive Logic Programming
    • Place of Presentation
      京都大学楽友会館
    • Year and Date
      2015-08-20
    • Related Report
      2015 Annual Research Report
    • Int'l Joint Research
  • [Presentation] SCSat3によるラムゼーグラフ探索について2015

    • Author(s)
      藤田 博
    • Organizer
      2015年度人工知能学会全国大会(第29回)
    • Place of Presentation
      公立はこだて未来大学
    • Year and Date
      2015-05-30
    • Related Report
      2015 Annual Research Report
  • [Presentation] Parallel Portfolio SATzilla20122015

    • Author(s)
      Aolong Zha, Ryuzo Hasegawa
    • Organizer
      人工知能学会 第97回人工知能基本問題研究会(SIG-FPAI)
    • Place of Presentation
      別府国際コンベンションセンター
    • Year and Date
      2015-03-22 – 2015-03-23
    • Related Report
      2014 Research-status Report
  • [Presentation] 節集合の簡単化によるMaxSATソルバーの高速化2015

    • Author(s)
      上村 直輝,越村 三幸,長谷川 隆三
    • Organizer
      人工知能学会 第97回人工知能基本問題研究会(SIG-FPAI)
    • Place of Presentation
      別府国際コンベンションセンター
    • Year and Date
      2015-03-22 – 2015-03-23
    • Related Report
      2014 Research-status Report
  • [Presentation] 重み付き部分MaxSAT問題における基数製薬符号化手法の改良2015

    • Author(s)
      早田 翔,長谷川 隆三
    • Organizer
      人工知能学会 第97回人工知能基本問題研究会(SIG-FPAI)
    • Place of Presentation
      別府国際コンベンションセンター
    • Year and Date
      2015-03-22 – 2015-03-23
    • Related Report
      2014 Research-status Report
  • [Presentation] MaxSATソルバを用いた帰納論理プログラミング2015

    • Author(s)
      力 規晃,越村 三幸,藤田 博,長谷川 隆三
    • Organizer
      人工知能学会 第97回人工知能基本問題研究会(SIG-FPAI)
    • Place of Presentation
      別府国際コンベンションセンター
    • Year and Date
      2015-03-22 – 2015-03-23
    • Related Report
      2014 Research-status Report
  • [Presentation] モデル生成型定理証明系とSATソルバー2015

    • Author(s)
      長谷川 隆三
    • Organizer
      人工知能学会 第97回人工知能基本問題研究会(SIG-FPAI)
    • Place of Presentation
      別府国際コンベンションセンター
    • Year and Date
      2015-03-22 – 2015-03-23
    • Related Report
      2014 Research-status Report
    • Invited
  • [Presentation] 帰納論理プログラミングを用いた化学実験支援2014

    • Author(s)
      力 規晃,越村 三幸,西田 光生,阿部 幸浩,藤田 博,長谷川 隆三
    • Organizer
      人工知能学会 第94回人工知能基本問題研究会(SIG-FPAI)
    • Place of Presentation
      根室市総合文化会館
    • Year and Date
      2014-07-24
    • Related Report
      2014 Research-status Report
  • [Presentation] 極小モデル生成とMaxSATソルバーについて2014

    • Author(s)
      長谷川 隆三
    • Organizer
      2014年度 人工知能学会全国大会(第28回)
    • Place of Presentation
      ひめぎんホール(愛媛県県民文化会館)
    • Year and Date
      2014-05-12 – 2014-05-15
    • Related Report
      2014 Research-status Report
    • Invited
  • [Presentation] 基数制約のSAT符号化を用いたMaxSATソルバーの試作2014

    • Author(s)
      越村 三幸,有村 寿高
    • Organizer
      2014年度 人工知能学会全国大会(第28回)
    • Place of Presentation
      ひめぎんホール(愛媛県県民文化会館)
    • Year and Date
      2014-05-12 – 2014-05-15
    • Related Report
      2014 Research-status Report
  • [Presentation] 高速SATソルバーZENN及びその高速化手法2014

    • Author(s)
      早田 翔,安本 猛,越村 三幸,藤田 博,長谷川 隆三
    • Organizer
      2014年度 人工知能学会全国大会(第28回)
    • Place of Presentation
      ひめぎんホール(愛媛県県民文化会館)
    • Year and Date
      2014-05-12 – 2014-05-15
    • Related Report
      2014 Research-status Report
  • [Presentation] MaxSATを利用したAES暗号鍵の復元2014

    • Author(s)
      廖暁鵑, 越村三幸
    • Organizer
      火の国情報シンポジウム
    • Place of Presentation
      大分大学工学部
    • Related Report
      2013 Research-status Report
  • [Presentation] SATソルバーの学習節を考慮した新高速化法2013

    • Author(s)
      早田 翔,長谷川 隆三,藤田 博,越村 三幸
    • Organizer
      2013年度 人工知能学会全国大会(第27回)
    • Place of Presentation
      富山国際会議場
    • Related Report
      2013 Research-status Report
  • [Presentation] SCSatを用いたラムゼー数の下界更新について2013

    • Author(s)
      藤田 博
    • Organizer
      2013年度 人工知能学会全国大会(第27回)
    • Place of Presentation
      富山国際会議場
    • Related Report
      2013 Research-status Report
  • [Presentation] MaxSATソルバ用いた高分子の組成と物性との関係に関する考察2013

    • Author(s)
      力 規晃,越村 三幸,西田 光生,阿部 幸浩,藤田 博,長谷川 隆三
    • Organizer
      2013年度 人工知能学会全国大会(第27回)
    • Place of Presentation
      富山国際会議場
    • Related Report
      2013 Research-status Report
  • [Remarks] QMaxSAT: Q-dai MaxSAT Solver

    • URL

      https://sites.google.com/site/qmaxsat/

    • Related Report
      2014 Research-status Report
  • [Remarks] QMaxSAT: Q-dai MaxSAT Solver

    • URL

      https://sites.google.com/site/qmaxsat/

    • Related Report
      2013 Research-status Report

URL: 

Published: 2014-07-25   Modified: 2019-07-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi