Memory Hierarchy Utilization of a SAT Solver

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Toggle side column

Memory Hierarchy Utilization of a SAT Solver

Studienarbeit von Norbert Mantehy
The project analyzes the hardware utilization of a SAT solver. The analysis is done

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.