Modern algorithms for the SAT problem reveal an almost tractable behavior on "real-world" instances. This is frequently assigned to the fact that these instances possess an internal "structure" that hard problem instances do not exhibit. However, little is known about this internal structure. We therfore propose the visualization of the instance's variable interaction graph as a first step of an empirical research program to analyze the internal problem structure. We present first results of such an analysis performed on instances of bounded model checking benchmark problems.