3.1.9. cnfformula.families.subgraph module¶

Implementation of formulas that check for subgraphs

BinaryCliqueFormula(G, k)¶

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. This formula uses the binary encoding, in the sense that the clique elements are indexed by strings of bits.

Parameters:	G : networkx.Graph a simple graph k : a non negative integer clique size
Returns:	a CNF object

class BinaryKCliqueCmdHelper¶

Bases: object

Command line helper for k-clique formula

Methods

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

static build_cnf(args)¶

Build a k-clique formula according to the arguments

Arguments: - args: command line options

description = 'Binary k clique formula'¶

name = 'kcliquebin'¶

static setup_command_line(parser)¶

Setup the command line options for k-clique formula

Arguments: - parser: parser to load with options.

CliqueFormula(G, k)¶

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 : networkx.Graph a simple graph k : a non negative integer clique size
Returns:	a CNF object

class KCliqueCmdHelper¶

Bases: object

Command line helper for k-clique formula

Methods

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

static build_cnf(args)¶

Build a k-clique formula according to the arguments

Arguments: - args: command line options

description = 'k clique formula'¶

name = 'kclique'¶

static setup_command_line(parser)¶

Setup the command line options for k-clique formula

Arguments: - parser: parser to load with options.

class RWCmdHelper¶

Bases: object

Command line helper for ramsey graph formula

Methods

`build_cnf`(args)	Build a formula to check that a graph is a ramsey number lower bound
`setup_command_line`(parser)	Setup the command line options for ramsey witness formula

static build_cnf(args)¶

Build a formula to check that a graph is a ramsey number lower bound

Arguments: - args: command line options

description = 'unsat if G witnesses that r(k,s)>|V(G)| (i.e. G has not k-clique nor s-stable)'¶

name = 'ramlb'¶

static setup_command_line(parser)¶

Setup the command line options for ramsey witness formula

Arguments: - parser: parser to load with options.

RamseyWitnessFormula(G, k, s)¶

Test whether a graph contains one of the templates.

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 : networkx.Graph a simple graph k : a non negative integer clique size s : a non negative integer independet set size
Returns:	a CNF object

class SubGraphCmdHelper¶

Bases: object

Command line helper for Graph Isomorphism formula

Methods

`build_cnf`(args)	Build a graph automorphism formula according to the arguments
`setup_command_line`(parser)	Setup the command line options for graph isomorphism formula

static build_cnf(args)¶

Build a graph automorphism formula according to the arguments

Arguments: - args: command line options

description = 'subgraph formula'¶

name = 'subgraph'¶

static setup_command_line(parser)¶

Setup the command line options for graph isomorphism formula

Arguments: - parser: parser to load with options.

SubgraphFormula(graph, templates, symmetric=False)¶

Test whether a graph contains one of the templates.

Given a graph \(G\) and a sequence of template graphs \(H_1\), \(H_2\), …, \(H_t\), the CNF formula claims that \(G\) contains an isomorphic copy of at least one of the template graphs.

E.g. when \(H_1\) is the complete graph of \(k\) vertices and it is the only template, the formula claims that \(G\) contains a \(k\)-clique.

Parameters:	graph : networkx.Graph a simple graph templates : list-like object a sequence of graphs. symmetric: all template graphs are symmetric wrt permutations of vertices. This allows some optimization in the search space of the assignments. induce: force the subgraph to be induced (i.e. no additional edges are allowed)
Returns:	a CNF object