Lightweight Dynamic Simplification Techniques for CDCL Solvers

DOI Web Site
  • SUGIMOTO Takuya
    Computer Science and Media Engineering,Department of Education Interdisciplinary Graduate School of Medicine and Engineering,University of Yamanashi
  • NABESHIMA Hidetomo
    Department of Research Interdisciplinary Graduate School of Medicine and Engineering, University of Yamanashi

Bibliographic Information

Other Title
  • CDCLソルバーのための軽量動的簡単化手法
  • CDCL ソルバー ノ タメ ノ ケイリョウ ドウテキ カンタンカ シュホウ

Search this article

Description

<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>

Journal

Details 詳細情報について

Report a problem

Back to top