3.1.10. cnfgen.families.subgraph module

Implementation of formulas that check for subgraphs

BinaryCliqueFormula(G, k, symbreak=True)

Test whether a graph has a k-clique (binary encoding)

Given a graph \(G\) and a non negative value \(k\), the CNF formula claims that \(G\) contains a \(k\)-clique. This formula uses the binary encoding, in the sense that the clique elements are indexed by strings of bits.

Parameters:

G : cnfgen.Graph

a simple graph

k : a non negative integer

clique size

symbreak: bool

force mapping to be non decreasing

Returns:

a CNF object

CliqueFormula(G, k, symbreak=True)

Test whether a graph has a k-clique.

Given a graph \(G\) and a non negative value \(k\), the CNF formula claims that \(G\) contains a \(k\)-clique.

Parameters:

G : cnfgen.Graph

a simple graph

k : a non negative integer

clique size

symbreak: bool

force mapping to be non decreasing

Returns:

a CNF object

RamseyWitnessFormula(G, k, s, symbreak=True)

True if graph contains either k-clique or and s independent set

Given a graph \(G\) and a non negative values \(k\) and \(s\), the CNF formula claims that \(G\) contains a neither a \(k\)-clique nor an independet set of size \(s\).

Parameters:

G : cnfgen.Graph

a simple graph

k : a non negative integer

clique size

s : a non negative integer

independet set size

symbreak: bool

force mapping to be non decreasing

Returns:

a CNF object

SubgraphFormula(G, H, induced=False, symbreak=False)

Test whether a graph has a k-clique.

Given two graphs \(H\) and \(G\), the CNF formula claims that \(H\) is an (induced) subgraph of \(G\).

Parameters:

G : cnfgen.Graph

a simple graph

H : cnfgen.Graph

the candidate subgraph

induced: bool

test for induced containment

symbreak: bool

force mapping to be non decreasing (this makes sense only if \(T\) is symmetric)

Returns:

a CNF object

non_edges(G)