3.1.2. cnfformula.families.coloring module

Formulas that encode coloring related problems

class ECCmdHelper

Bases: object

Methods

build_cnf
setup_command_line

static build_cnf(args)

description = 'even coloring formulas'

name = 'ec'

static setup_command_line(parser)

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]	(1, 2) 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 : networkx.Graph

a simple undirected graph

colors : list or positive int

a list of colors or a number of colors

Returns:

CNF

the CNF encoding of the coloring problem on graph G

class KColorCmdHelper

Bases: object

Command line helper for k-color formula

Methods

build_cnf(args)	Build a k-colorability formula according to the arguments
setup_command_line(parser)	Setup the command line options for k-color formula

static build_cnf(args)

Build a k-colorability formula according to the arguments

Arguments: - args: command line options

description = 'k-colorability formula'

name = 'kcolor'

static setup_command_line(parser)

Setup the command line options for k-color formula

Arguments: - parser: parser to load with options.