\(<< GrafPack`Master`
\)
\(\(VariableName[eds_, 
          e_] := \(Flatten[
            Position[eds, 
              e]]\)[\([\)\(1\)\(]\)];\)
\)
IncidentEdges[g_, v_] := 
        Map[Sort[{v, #}] &, Neighbours[g, v]];

\(\(VariableSetToClauses[{s1_, 
            s2_}] := 
\(({
{\(-a\), \(-b\)}, 
{a, b}
} /. {a -> s1, 
              b -> s2})\);\)
\)
VariableSetToClauses[{s1_, s2_, s3_, 
            s4_}] := 
({
{-a, -b, -c, -d}, 
{-a, -b, -c, 
                d}, 
{-a, -b, 
                c, -d}, 
{-a, 
                b, -c, -d}, 
{-a, b, c, 
                d}, 
{a, -b, -c, -d}, 
{a, -b, c, d}, 
{a, b, -c, 
                d}, 
{a, b, 
                c, -d}, 
{a, b, c, 
                d}
} /. {a -> s1, b -> s2, 
              c -> s3, 
              d -> 
                s4}
);

\(\(GraphToCNF[
          g_] := 
Module[{eds, clauses = {}, 
            loc}, 
eds = 
            ToEdges[g]; 
Do[
loc = 
              Map[VariableName[eds, #] &, 
                IncidentEdges[g, v]]; 
clauses = 
              Join[clauses, 
                VariableSetToClauses[loc]]; 
, {v, 1, 
              Order[g]}
]; 
clauses
];\)
\)
\(\(ClauseToString[cl_] := 
        StringJoin[
          Append[Map[\((ToString[#] <> " ")\) &, 
              cl], " 0"]];\)
\)
\(\(WriteCNF[name_, 
          cnf_] := 
Module[{fil, 
            s}, 
fil = 
            OpenWrite[name]; 
WriteString[
            fil, 
"p   cnf   " <> 
              ToString[Max[cnf]] <> "   " <> 
              ToString[
                Length[cnf]] <> " 
"
]; 
Do[
s = 
              ClauseToString[
                cnf[\([\)\(i\)\(]\)]]; 
WriteString[fil, 
              s <> "
"]; 
, {i, 1, 
              Length[cnf]}
]; 
Close[
            fil]; 
];\)\)

\(\(\(
\)\( (*
Even\ edge\ colouring\ of\ a\ 4 - 
        regular\ eulerian\ graph\ with\ one\ subdivided\ edge; 
Unsatisfiable
*) \)\(
\)\(
\)\(\(g = 
        ReadGraph["./cagesk4g06.g6", 
          Graph6];\)


    \(e = First[ToEdges[g]];\)

    \(g2 = SubdivideEdge[g, e];\)

    \(cnf = GraphToCNF[g2];\)


    Length[cnf]

    Size[g]


    WriteCNF["test.cnf", cnf]\)\)\)