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

2019 Fiscal Year Final Research Report

A fast Boolean satisfiability problem solver by shortening the proof

Research Project

  • PDF
Project/Area Number 17K00300
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Intelligent informatics
Research InstitutionUniversity of Yamanashi

Principal Investigator

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

Project Period (FY) 2017-04-01 – 2020-03-31
Keywords充足可能性判定(SAT)問題 / SATソルバー / 決定的並列SATソルバー / 圧縮
Outline of Final Research Achievements

In order to improve the performance of propositional satisfiability problem solver (SAT solver), we have implemented a deterministic portfolio parallel SAT solver and a solver that can directly solve a compressed instance. The former parallel SAT solver ensures reproducible behavior and achieves comparable performance with non-deterministic parallel solvers by allowing delayed clause exchange. The latter approach compresses regular clauses in a given SAT instance and can solve the compressed instance without expansion. We have experimentally confirmed that this approach is effective to solve the huge SAT instances. Although this has no effect for proof shortening at the moment, it will be the foundation of the study to acquire compressed learned clauses.

Free Research Field

制約充足処理系の設計・開発

Academic Significance and Societal Importance of the Research Achievements

SAT問題は,計算機科学において最も基本的かつ本質的な組合せ問題であり,SAT問題を解くソルバーは様々な応用領域における基盤推論技術として幅広く利用されている.よってSATソルバーの高速化は,それを基盤とする様々な応用領域にとって重要である.我々の考案した遅延学習節交換法に基づく並列SATソルバーは,再現性のある挙動を保証しているため並列SATソルバーの実応用を容易にする.また巨大なSAT問題を圧縮したまま解く手法の開発は,SATの応用範囲の拡大のために重要であり,圧縮節の学習による証明短縮手法を検討するための基盤となる.

URL: 

Published: 2021-02-19  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi