Constraint Graph: Long Multiplication
This is a picture of the logical structure of a problem in
bounded model checking, as represented to a propositional
satisfiability (SAT) solver. The actual problem is to
verify that two algorithms for computing multiplication of
16-bit integers give the same results. The colours are
assigned to the 2395 boolean variables according to their
names - see the legend. The user of the constraint graph
viewer can choose to display this particular graph with
different colours assigned to each of the 16 bits, or with
different colours representing different iterations of the
loop.
The
force-directed layout
used to draw these graphs is based on a standard spring
and charged particle metaphor. We use springs with a rest
length of zero, meaning that the edges exert simply an
attraction, no matter how close the vertices get. The
effect is that related variables are drawn close together
and unrelated ones far apart. In order to get the layout
to converge in reasonable time, we use an initial
hierarchical clustering phase to seed the layout and then
a quad tree decomposition algorithm to compute a
reasonable approximation to a low-energy state in
O(n.log(n)) time per iteration instead of the
O(n2) required by naive
methods. A "temperature" setting under user control helps
to force convergence. The user also decides when to
terminate the layout process.
The physical metaphor, closely related to the reality of
many natural processes, can result in forms which are
quasi-organic in appearance, despite their origin in the
most hard-edged of logical problems.
|