SAT問題を解くDPLLベースの探索法に対する改善手法  [in Japanese] An Improvement for DPLL-based SAT solvers  [in Japanese]

Search this Article

Author(s)

Abstract

近年SATソルバーは実用性の面で需要があり,その需要に答えるべく,ここ10年ほどで飛躍的な進歩を遂げている.実用性の高いSATソルバーの殆んどはDPLLアルゴリズムをベースにしている.近年のDPLLベースのアルゴリズムは,仮定に仮定を重ね,探索中に矛盾を導いては,それを回避するための制約条件を積極的に学習することによって探索範囲を狭める仕組みになっている. DPLLではある種の制約条件を学習する際に,今までの探索を放棄して,一旦rootまでbacktrackすることになっている.しかし実用的には,いつもrootまでbacktrackするのが良いとは限らない.そこで本論文では,あるヒューリスティックスに従って途中までbacktrackするような手法を提案する.その種の制約条件を全く学習できなければ,従来法と全く同じ振る舞いになるので,従来法に比べて大きな欠点はない.

Recent SAT solvers have drastically improved their performance in this decade. Recent DPLL-based algorithm makes a series of assumptions which leads to a conflict. By learning a constraint to aviod the conflict, the search space is narrowed. DPLL discards a current search and backtracks to the root level when learning a certain kind of constraints. However it is not always the best choice to backtrack to the root. We introduces a method to backtrack to a midstream level by a simple heristics.

Journal

  • IPSJ SIG Notes

    IPSJ SIG Notes 63, 41-44, 2007-03-03

    Information Processing Society of Japan (IPSJ)

References:  8

Codes

  • NII Article ID (NAID)
    110006248718
  • NII NACSIS-CAT ID (NCID)
    AN10505667
  • Text Lang
    JPN
  • Article Type
    ART
  • ISSN
    09196072
  • NDL Article ID
    8706361
  • NDL Call No.
    Z14-1121
  • Data Source
    CJP  NDL  NII-ELS 
Page Top