Some Simple Lossy Translations

There are a number of relationships in a SAT instance that could be represented by a graph, and variations on these are also possible. This section defines some basic translations that partially capture some of these relationships:

cooccurrence of variables

The graph of the cooccurrence of variables is defined as a graph, $G = (V,E)$, with $V$ as the set of vertices that directly correspond to the set of variables in the SAT instance, and $E$ as the set of edges defined as follows: for each clause $c$ in the SAT instance if $c$ contains the variable $v_i$ and the variable $v_j$ then there is an edge from the vertex $v_{v_i}$ to vertex $v_{v_j}$.

cooccurrence of literals

The graph of the cooccurrence of literals is defined as a graph, $G = (V,E)$, with $V$ as the set of vertices that directly correspond to the set of literals in the SAT instance, and $E$ as the set of edges defined as follows: for each clause $c$ in the SAT instance if $c$ contains the literal $l_i$ and the literal $l_j$ then there is an edge from the vertex $v_{l_i}$ to vertex $v_{l_j}$.

simple implicational relations

The graph of simple implicational relations is defined as a graph, $G = (V,E)$, with $V$ as the set of vertices that directly correspond to the set of literals in the SAT instance, and $E$ as the set of edges defined as follows: each clause $c = (l_1 \vee l_2 \vee \ldots \vee l_k)$ in the SAT instance is interpreted as an implicational statement $(\neg{l_1} \vee \neg{l_2} \vee \ldots \vee l_k)$ and there are directed edges from the vertex $v_{\neg{l_i}}$ to $v_{\neg{l_{i+1}}}$ for $0<i<k-2$ (when $k>2$) and the directed edge $v_{\neg{l_{k-1}}}$ to $v_{l_{k}}$ (when $k>1$). Note that the edges are defined in the input order of the literals in a clause.

all possible implicational relations

The graph of all possible implicational relations is equivalent to the basic version, but instead of generating a linear number of edges based on the the input order it generates edges for every possible implicational relation that arises from each clause. For a clause of size $k$ there are $(k-1)(k-2) + k(k-1)$ edges. A SAT instances with many large clauses means the resulting graph size may be too large to adequately visualise.