implication_graph.dot

digraph sat2 {
//implication graph
rankdir=LR;
node[width=0]

#{¬xvy}, {¬yvz}, {¬zvw} ,{¬wvu},{¬uv¬x},{xvw},{¬wvx}

nx[label="-x"];
ny[label="-y"];
nz[label="-z"];
nu[label="-u"];
nw[label="-w"];

x -> y;
ny -> nx;

y -> z;
nz -> y;

z -> w;
nw -> nz;

w -> u;
nu -> nw;

u -> nx;
x -> nu;

#{xvw},{¬wvx}

nx -> w;
nw -> x;

w -> x;
nx -> nw;
}
        

SE2satimplicationgraph

http://cs.stackexchange.com/questions/16311/2-sat-proof-with-boolean-literals

strongly_connected_components.dot

digraph sat2 {
//strongly connected component
rankdir=LR;
node[width=0]

#{¬xvy}, {¬yvz}, {¬zvw} ,{¬wvu},{¬uv¬x},{xvw},{¬wvx}

nx[label="-x"];
nz[label="-z"];
nu[label="-u"];
nw[label="-w"];

x -> y;

y -> z;
nz -> y;

z -> w;
nw -> nz;

w -> u;
nu -> nw;

u -> nx;
x -> nu;

#{xvw},{¬wvx}

nx -> w;
nw -> x;

w -> x;
nx -> nw;
}