Improving resource-unaware SAT solvers

Steffen Hölldobler, Norbert Manthey, Ari Saptawijaya

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Citations (Scopus)

Abstract

The paper discusses cache utilization in state-of-the-art SAT solvers. The aim of the study is to show how a resource-unaware SAT solver can be improved by utilizing the cache sensibly. The analysis is performed on a CDCL-based SAT solver using a subset of the industrial SAT Competition 2009 benchmark. For the analysis, the total cycles, the resource stall cycles, the L2 cache hits and the L2 cache misses are traced using sample based profiling. Based on the analysis, several techniques - some of which have not been used in SAT solvers so far - are proposed resulting in a combined speedup up to 83% without affecting the search path of the solver. The average speedup on the benchmark is 60%. The new techniques are also applied to MiniSAT2.0 improving its runtime by 20% on average.

Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings
EditorsChristian G. Fermuller
Pages519-534
Number of pages16
DOIs
Publication statusPublished - 23 Nov 2010
Event17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17 - Yogyakarta, Indonesia
Duration: 10 Oct 201015 Oct 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6397 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17
CountryIndonesia
CityYogyakarta
Period10/10/1015/10/10

Fingerprint Dive into the research topics of 'Improving resource-unaware SAT solvers'. Together they form a unique fingerprint.

  • Cite this

    Hölldobler, S., Manthey, N., & Saptawijaya, A. (2010). Improving resource-unaware SAT solvers. In C. G. Fermuller (Ed.), Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings (pp. 519-534). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6397 LNCS). https://doi.org/10.1007/978-3-642-16242-8-37