3.1.3. cnfgen.families.graphisomorphism module

Graph isomorphimsm/automorphism formulas

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, nontrivial=False)

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

nontrivial: bool

forbid identical mapping

Returns:

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

are isomorphic.