Memory Hierarchy Utilization of a SAT Solver
Memory Hierarchy Utilization of a SAT Solver
project thesis by Norbert Mantehy
- Supervisor Steffen Hölldobler, Hermann Härtig
- Wissensverarbeitung
- 31 März 2010 – 31 März 2010
- Download
using statistical profiling and tracing the following processor events: total cycles, resource
stall cycles, level 2 cache hits and level 2 cache misses. The HPC Toolkit is used
to perform the analysis on top of the PAPI library. The used benchmark is a part of
the SAT competition 2009 application benchmark.
The analysis has additionally been done on two well known solver MiniSAT and PrecoSAT
and unveiled similar utilization problems as in the project SAT solver. Its result
is that the utilization can be increased for example by improving the clause representation,
using the prefetch unit of the CPU and maintaining frequently used data structures
lazily. The combination of the suggested improvements speed up the project SAT solver
by 60%. The runtime improvement is mainly caused by fewer main memory and level 2
cache accesses.
