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

A study on deterministic parallel SAT solvers

Research Project

Project/Area Number 20K11934
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 61030:Intelligent informatics-related
Research InstitutionUniversity of Yamanashi

Principal Investigator

Nabeshima Hidetomo  山梨大学, 大学院総合研究部, 准教授 (10334848)

Project Period (FY) 2020-04-01 – 2023-03-31
Project Status Completed (Fiscal Year 2022)
Budget Amount *help
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2022: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2021: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2020: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
Keywords充足可能性判定(SAT)問題 / SATソルバー / 決定的並列SATソルバー / 充足可能性判定(SAT)問題 / 決定的SATソルバー / 並列SATソルバー / 決定的並列SAT解法
Outline of Research at the Start

命題論理の充足可能性判定問題(SAT)を解くソルバーは,システム検証やプランニング,スケジューリングなど実社会における様々な応用領域の基盤推論技術として幅広く利用されている.複数のCPUやPCを利用してSAT問題を並列に解く並列SATソルバーはSAT問題の強力な解決法であるが,ほとんどの並列SATソルバーは実行結果に再現性がなく,安定性・頑健性に欠けるという実用上の課題がある.本研究では実社会における並列SATソルバーの応用を促進するため,我々が考案した遅延学習節交換法に基づく決定的な振る舞いをする並列SATソルバーの高速化ならびに高機能化の実現を目指す.

Outline of Final Research Achievements

SAT (propositional satisfiability testing) solvers are widely used as a fundamental reasoning technique in various application domains such as system verification, planning and scheduling. In order to achieve fast solving of SAT instances, this research has developed a framework for a shared-memory deterministic parallel SAT solver. It ensures reproducible behaviour, which is important for the practical application of parallel SAT solvers, and allows existing fast sequential SAT solvers to be parallelised with less effort. Our solver has won prizes in several categories in the parallel track of the International SAT Competition 2022, showing performance comparable to non-deterministic parallel SAT solvers.

Academic Significance and Societal Importance of the Research Achievements

SAT問題の高速解法は,それを推論技術として利用する様々な応用分野にとって重要である.これまで並列SATソルバーのほとんどは求解の効率を優先するため再現性のある挙動の担保ができていなかった.これは例えばシステム検証では実行のたびに異なる不具合が見つかることを意味し,実応用に向けた課題の1つであった.我々が開発した決定的並列SATソルバーのためのフレームワークは,再現性のある挙動を担保しつつ,既存の逐次SATソルバーを少ない手間で並列化することが可能である.このフレームワークは既存の非決定的並列SATソルバーに匹敵する性能を示しており,並列SATソルバーの実用化にむけた基盤となるものといえる.

Report

(4 results)
  • 2022 Annual Research Report   Final Research Report ( PDF )
  • 2021 Research-status Report
  • 2020 Research-status Report
  • Research Products

    (9 results)

All 2022 2021 2020 Other

All Journal Article (2 results) (of which Peer Reviewed: 2 results,  Open Access: 1 results) Presentation (4 results) Remarks (3 results)

  • [Journal Article] DPS: A Framework for Deterministic Parallel SAT Solvers2022

    • Author(s)
      H. Nabeshima, T. Fukiage, Y. Obitsu, X. Lu, K. Inoue
    • Journal Title

      The 12th International Workshop on Pragmatics of SAT

      Pages: 1-15

    • Related Report
      2022 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Reproducible Efficient Parallel SAT Solving2020

    • Author(s)
      Nabeshima Hidetomo、Inoue Katsumi
    • Journal Title

      Theory and Applications of Satisfiability Testing - SAT 2020, LNCS

      Volume: 12178 Pages: 123-138

    • DOI

      10.1007/978-3-030-51825-7_10

    • ISBN
      9783030518240, 9783030518257
    • Related Report
      2020 Research-status Report
    • Peer Reviewed
  • [Presentation] 決定的並列SATソルバー構築のための汎用フレームワークの検討2022

    • Author(s)
      吹上 翼, 帯津 勇斗, 鍋島 英知, 盧 暁南
    • Organizer
      第36回人工知能学会全国大会
    • Related Report
      2022 Annual Research Report
  • [Presentation] 圧縮した SAT 問題における高速な単位伝播手法2021

    • Author(s)
      早瀬 悠真, 鍋島 英知, 盧 暁南
    • Organizer
      第35回人工知能学会全国大会
    • Related Report
      2021 Research-status Report
  • [Presentation] Towards CEGAR-Based Parallel SAT Solving2021

    • Author(s)
      Takehide Soh, Hidetomo Nabeshima, Mutsunori Banbara, Naoyuki Tamura, Katsumi Inoue
    • Organizer
      Pragmatics of SAT
    • Related Report
      2021 Research-status Report
  • [Presentation] 大規模な SAT 問題を圧縮したまま解くソルバーの開発2020

    • Author(s)
      早瀬 悠真, 鍋島 英知
    • Organizer
      第34回人工知能学会全国大会
    • Related Report
      2020 Research-status Report
  • [Remarks] DPS-Kissat

    • URL

      https://github.com/nabesima/DPS-satcomp2023

    • Related Report
      2022 Annual Research Report
  • [Remarks] DPS - 決定的並列SATソルバーのためのフレームワーク

    • URL

      https://github.com/nabesima/DPS-pos2022

    • Related Report
      2022 Annual Research Report
  • [Remarks] ManyGlucose 4.1-60

    • URL

      https://github.com/nabesima/manyglucose-satcomp2020

    • Related Report
      2020 Research-status Report

URL: 

Published: 2020-04-28   Modified: 2024-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi