For the following graph, I can easily setup clauses that use variables $E_{0,3}$, $E_{1,3}$, and $E_{2,3}$ for the 3 potential new edges, so that a SAT solver can find all the graphs that are 3-colorable.
My SAT condition is actually doing 2 things:
- choose a configuration for the edges
- and find a 3-color solution for the graph that takes the edge configuration into account
What transformation can I apply to the clauses so that the condition is the opposite one: find a graph that is not 3-colorable?
It feels a bit like: find a configuration for these 3 variables, such that this 3-color equation is not satisfiable. If I just invert the whole condition, the SAT solver will simply find a way to badly color the graph.