CDCLソルバーのための軽量動的簡単化手法

DOI Web Site

書誌事項

タイトル別名
  • Lightweight Dynamic Simplification Techniques for CDCL Solvers
  • CDCL ソルバー ノ タメ ノ ケイリョウ ドウテキ カンタンカ シュホウ

この論文をさがす

説明

<p>In this paper, we propose two techniques of the dynamic simplification algorithm for CDCL (conflict-driven clause learning) solvers. Firstly, We propose an extension of the dynamic subsumption algorithm proposed by Hamadi et al. The clause learning mechanism in CDCL solvers can be formalized as a resolution process. The dynamic subsumption efficiently checks whether a resolvent subsumes the parent clause or not. The subsumed clause can be removed. In this study, we extend the subsumption checking for ancestors. Secondly, We propose an extraction method of implicit binary clauses from the resolution process and show a lightweight subsumption checking method with these binary clauses. When using the clauses to check subsumptions by binary clauses. Because it is a binary clause, cost of inspection is low, the effect is high. The experimental results show that our techniques can improve the performace of a CDCL solver.</p>

収録刊行物

詳細情報 詳細情報について

問題の指摘

ページトップへ