TY - GEN
T1 - Improving resource-unaware SAT solvers
AU - Hölldobler, Steffen
AU - Manthey, Norbert
AU - Saptawijaya, Ari
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85037532947&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-16242-8_37
DO - 10.1007/978-3-642-16242-8_37
M3 - Conference contribution
AN - SCOPUS:85037532947
SN - 364216241X
SN - 9783642162411
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 519
EP - 534
BT - Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings
PB - Springer Verlag
ER -