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.


Dr J K Slaney                      Phone (Aus.):  (026) 125 8607
Automated Reasoning Project        Phone (Int.): +61 26 125 8607
Australian National University     Fax (Aus.):    (026) 125 8651
Canberra, ACT, 0200, AUSTRALIA     Fax (Int.):   +61 26 125 8651
John.Slaney@anu.edu.au