Conclusions

This study investigated some approaches for representing satisfiability problems for visualisation as a connected graph. Some domains of benchmark problems yielded interesting structural formations under some of these interpretations. The structure is visible enough that it warrants further investigation as to how these features may be exploited by a search algorithm. Most notable are the modularity, symmetry, and repetition that occur in difficult real world problems. In order to recognise such structure a search algorithm may have to use partitioning, learning, or unification as adjunct techniques to enhance current search methods.

Not all benchmark problems that we generated graphs for were as interesting as the ones presented here. The methods used to visualise these problems are fairly simple, and the challenge of finding representations of satisfiability problems for meaningful visualisation continues.