An Improved Hybrid SAT Solver for Bounded Model Checking in Circuit Design

DOI

10.2991/iccnce.2013.70How to use a DOI?

Keywords

BMC, SAT, DPLL, WalkSAT, adaptive noise

Abstract

Model checking is one of main formal verification methods that are used in the process of circuit design and verification. However, there is a problem of state memory explosion in traditional model checking methods. Bounded model checking (BMC), in which the Davis-Putnam-Logemann-Loveland (DPLL) algorithm based Satisfiability (SAT) solver is used to verify the circuits, can avoid this problem, whereas, its efficiency depends on the performance of the solver. Hybrid SAT solver combines the advantages of the completeness of DPLL and the fast solving property of stochastic local search algorithm, e.g. WalkSAT, and is proved to be an efficient improving way. However, it is noted that the noise parameter in WalkSAT could affect the solver’s overall performance. In this paper, an adaptive noise mechanism is proposed to integrate with the hybrid algorithm framework to further improve the solver’s performance. Our experimental results have shown that the designed hybrid solver with adaptive noise performs well in BMC instances and some other circuits.

Copyright

© 2013, the Authors. Published by Atlantis Press.

Open Access

This is an open access article distributed under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).

Download article (PDF)

TY  - CONF
AU  - Yuesheng Zhu
AU  - Deke Yu
PY  - 2013/07
DA  - 2013/07
TI  - An Improved Hybrid SAT Solver for Bounded Model Checking in Circuit Design
BT  - Proceedings of the International Conference on Computer, Networks and Communication Engineering (ICCNCE 2013)
PB  - Atlantis Press
SP  - 282
EP  - 285
SN  - 1951-6851
UR  - https://doi.org/10.2991/iccnce.2013.70
DO  - 10.2991/iccnce.2013.70
ID  - Zhu2013/07
ER  -