インクリメンタルSAT解法ライブラリとその応用  [in Japanese] An Incremental SAT Solving Library and its Applications  [in Japanese]

Access this Article

Search this Article

Author(s)

    • 迫 龍哉 SAKO Tatsuya
    • 神戸大学大学院システム情報学研究科 Graduate School of System Informatics, Kobe University
    • 鍋島 英知 NABESHIMA Hidetomo
    • 山梨大学大学院医学工学総合研究部 Department of Research Interdisciplinary, Graduate School of Medicine and Engineering, University of Yamanashi
    • 井上 克巳 INOUE Katsumi
    • 国立情報学研究所情報学プリンシプル研究系|総合研究大学院大学複合科学研究科情報学専攻|東京工業大学大学院情報理工学研究科計算工学専攻 Principles of Informatics Research Division, National Institute of Informatics|Department of Informatics, School of Multidisciplinary Sciences, SOKENDAI (The Graduate University for Advanced Studies)|Department of Computer Science, Graduate School of Information Science and Engineering, Tokyo Institute of Technology

Abstract

近年,命題論理の充足可能性判定(SAT)問題を解くSATソルバーの飛躍的な性能向上を背景に,問題をSATに変換し,SATソルバーを用いて求解するSAT型ソルバーが成功を収めている.しかしながら,最適化問題,解列挙問題などに対しては,SATソルバーを複数回起動する必要があり,求解性能が大きく低下することがある.この問題を解決する方法として,インクリメンタルSAT解法の利用が挙げられる.SATソルバー競技会のひとつであるSAT Race 2015で,このような解法を容易に実現するためのインクリメンタルSAT APIが提案された.本論文では,それを拡張したインクリメンタルSAT APIであるiSATを提案し,その応用について述べる.提案する拡張により,問題を簡潔に記述でき,Javaからの利用も可能になる.また,ショップスケジューリング問題,N-クイーン問題,ハミルトン閉路問題に対する実験結果を通じ,iSAT利用の有効性を示す.

Remarkable improvements on SAT solvers over the last decade have led the success of SAT-based solvers. However, existing SAT-based solvers cannot efficiently solve optimization and enumeration problems since those solvers invoke SAT solvers multiple times from scratch and do not reuse search information such as learnt clauses. Recently, incremental SAT method has been proposed to efficiently solve these problems. In addition, such incremental SAT API is proposed in SAT Race 2015. In this paper, we propose iSAT, an extended incremental SAT API, and describe its application. This proposed API allows users to implement SAT-based systems concisely and within Java. We show the effectiveness of using iSAT through experimental results on shop-scheduling, N-queens, and Hamiltonian cycle problems.

Journal

  • Computer Software

    Computer Software 33(4), 4_16-4_29, 2016

    Japan Society for Software Science and Technology

Codes

  • NII Article ID (NAID)
    130005290581
  • NII NACSIS-CAT ID (NCID)
    AN10075819
  • Text Lang
    JPN
  • ISSN
    0289-6540
  • NDL Article ID
    027737439
  • NDL Call No.
    Z14-1033
  • Data Source
    NDL  J-STAGE 
Page Top