Towards Lightweight Satisfiability Solvers for Self-Verification

Fritjof Bornebusch, Robert Wille, Rolf Drechsler

In: 7th International Symposium on Embedded Computing and System Design. International Symposium on Electronic System Design (ISED-17) 7th December 18-20 Durgapur India 2017.


Solvers for Boolean satisfiability (SAT solvers) are essential for various hardware and software verification tasks such as equivalence checking, property checking, coverage analysis, etc. Nevertheless, despite the fact that very power- ful solvers have been developed in the recent decades, this progress often still cannot cope with the exponentially increas- ing complexity of those verification tasks. As a consequence, researchers and engineers are investigating complementarily different verification approaches which require changes in the core methods as well. Self-verification is such a promising approach where e.g. SAT solvers have to be executed on the system itself. This comes with hardware restrictions such as limited memory and motivates lightweight SAT solvers. This work provides a case study towards the development of such solvers. To this end, we consider several core techniques of SAT solvers (such as clause learning, Boolean constraint propaga- tion, etc.) and discuss as well as evaluate how they contribute to both, the run-time performance but also the required memory requirements. The findings from this case study provide a basis for the development of dedicated, i.e. lightweight, SAT solvers to be used in self-verification solutions.


ised2017_towards_lightweight_sat_solvers.pdf (pdf, 226 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence