3.1.11. cnfformula.families.cliquecoloring module

Implementation of the clique-coloring formula

CliqueColoring(n, k, c)

Clique-coloring CNF formula

The formula claims that a graph \(G\) with \(n\) vertices simultaneously contains a clique of size \(k\) and a coloring of size \(c\).

If \(k = c + 1\) then the formula is clearly unsatisfiable, and it is the only known example of a formula hard for cutting planes proof system. [1]

Variables \(e_{u,v}\) to encode the edges of the graph.

Variables \(q_{i,v}\) encode a function from \([k]\) to \([n]\) that represents a clique.

Variables \(r_{v,\ell}\) encode a function from \([n]\) to \([c]\) that represents a coloring.

Parameters:

n : number of vertices in the graph

k : size of the clique

c : size of the coloring

Returns:

A CNF object

References

[1]	(1, 2) Pavel Pudlak. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic (1997)

class CliqueColoringCmdHelper

Bases: object

Command line helper for the Clique-coclique CNF

Methods

build_cnf(args)	Build a Clique-coclique formula according to the arguments
setup_command_line(parser)	Setup the command line options for clique-coloring formula

static build_cnf(args)

Build a Clique-coclique formula according to the arguments

Arguments: - args: command line options

description = 'There is a graph G with a k-clique and a c-coloring'

name = 'cliquecoloring'

static setup_command_line(parser)

Setup the command line options for clique-coloring formula

Arguments: - parser: parser to load with options.