3.1.2. cnfgen.families.coloring module

Formulas that encode coloring related problems

EvenColoringFormula(G)

Even coloring formula

The formula is defined on a graph \(G\) and claims that it is possible to split the edges of the graph in two parts, so that each vertex has an equal number of incident edges in each part.

The formula is defined on graphs where all vertices have even degree. The formula is satisfiable only on those graphs with an even number of vertices in each connected component [1].

Returns:

CNF object

Raises:

ValueError

if the graph in input has a vertex with odd degree

References

[1]	Locality and Hard SAT-instances, Klas Markstrom Journal on Satisfiability, Boolean Modeling and Computation 2 (2006) 221-228

GraphColoringFormula(G, colors, functional=True)

Generates the clauses for colorability formula

The formula encodes the fact that the graph \(G\) has a coloring with color set colors. This means that it is possible to assign one among the elements in ``colors``to that each vertex of the graph such that no two adjacent vertices get the same color.

Parameters:

G : cnfgen.Graph

a simple undirected graph

colors : non negative int

the number of colors

functional: bool

forbid a vertex to be mapped to multiple colors

Returns:

CNF

the CNF encoding of the coloring problem on graph G