3.1.3. cnfformula.families.graphisomorphism module

Graph isomorphimsm/automorphism formulas

class GAutoCmdHelper

Bases: object

Command line helper for Graph Automorphism 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 automorphism formula

static build_cnf(args)

Build a graph automorphism formula according to the arguments

Arguments: - args: command line options

description = 'graph automorphism formula'

name = 'gauto'

static setup_command_line(parser)

Setup the command line options for graph automorphism formula

Arguments: - parser: parser to load with options.

class GIsoCmdHelper

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 = 'graph isomorphism formula'

name = 'giso'

static setup_command_line(parser)

Setup the command line options for graph isomorphism formula

Arguments: - parser: parser to load with options.

GraphAutomorphism(G)

Graph Automorphism formula

The formula is the CNF encoding of the statement that a graph G has a nontrivial automorphism, i.e. an automorphism different from the idential one.

Returns:

A CNF formula which is satiafiable if and only if graph G has a

nontrivial automorphism.

GraphIsomorphism(G1, G2)

Graph Isomorphism formula

The formula is the CNF encoding of the statement that two simple graphs G1 and G2 are isomorphic.

Parameters:

G1 : networkx.Graph

an undirected graph object

G2 : networkx.Graph

an undirected graph object

Returns:

A CNF formula which is satiafiable if and only if graphs G1 and G2

are isomorphic.