next up previous
Next: Some Simple Lossy Translations Up: Visualisation of Satisfiability Problems Previous: Visualisation of Satisfiability Problems

Translating SAT Instances to a Connected Graph

Visualisation of search may help us understand how to interact with and improve the problem specification and the problem solving processes. Interpreting a satisfiability (SAT) problem as a connected graph can give some idea about the structure or nature of the problem. Visualisation of SAT problems may also help us further understand specific problem domains.

It is possible to translate an instance of SAT instance to an instance of some other NP-Complete problem that takes a connected graph as the input, for example Graph Colouring (a translation appears in [2]. However, such a translation can encode structure that represents the translation itself, rather than the original SAT instance. Complete preservation of the logical specification of the original instance is not necessary for visualisation. Visualisation of the problem only aspires to capturing some relevant and informative aspects of the problem, for example the internal structures.

Representing a SAT instance as a graph for visualisation can be a lossy procedure For example, the cooccurrence of variables in a SAT instance can be represented as a graph with a vertex representing each variable and an edge between two vertices when those variables occur together in a clause. The trade off with a lossy representation is information - some aspects are captured and some are lost. The translation chooses to represent some possibly meaningful aspect of the instance in a succinct way, and therefore will always be bias toward the information it is concerned with. The process of experimenting with various translations searches for a useful or meaningful visual representation. The use of lossy translations for other purposes, such as topological analysis, is exposed to the problem that the translation may not be entirely appropriate for the actual analysis i.e. the translated instance must contain a good representation of the information that any further analysis will rest upon. In Section 2 it is illustrated that similar translations can produce very different topological results.



Subsections
next up previous
Next: Some Simple Lossy Translations Up: Visualisation of Satisfiability Problems Previous: Visualisation of Satisfiability Problems
Last modified: 2004-03-17
Andrew Slater