https://en.wikipedia.org/wiki/Graph_theory

introduction to graph theory - grinberg Infinite graphs? How does this even make sense.

graph theory vids

https://en.wikipedia.org/wiki/Line_graph

https://en.wikipedia.org/wiki/Strongly_connected_component#Definitions Condensation graph - strongly connected component collapsed to vertex

https://en.wikipedia.org/wiki/List_of_graphs particular graphs

https://en.wikipedia.org/wiki/Multigraph multiple edges between vertices https://en.wikipedia.org/wiki/Directed_graph directed edges https://en.wikipedia.org/wiki/Rooted_graph graph with distinguished root. “flow graphs”. Aczel’s anti foundation axiom https://en.wikipedia.org/wiki/Directed_acyclic_graph https://en.wikipedia.org/wiki/Graph_labeling

https://en.wikipedia.org/wiki/Hypergraph edges connect more than one vertex https://github.com/pnnl/HyperNetX https://github.com/yamafaktory/hypergraph

Drags: A Simple Algebraic Framework For Graph Rewriting

Egraphs :)

Reinhard Diestel - Graph Theory

Graph Families / Classes

https://en.wikipedia.org/wiki/Category:Graph_families

https://en.wikipedia.org/wiki/Complete_graph totally connected

https://en.wikipedia.org/wiki/Regular_graph Every vertex has same number of neighbors

https://en.wikipedia.org/wiki/Perfect_graph

https://en.wikipedia.org/wiki/Permutation_graph

https://en.wikipedia.org/wiki/Cograph indcutively generated by disojint union and complement

https://en.wikipedia.org/wiki/Distance-hereditary_graph

https://en.wikipedia.org/wiki/Chordal_graph all cycles of 4 or more vertices have a chord

series parallel graph

https://en.wikipedia.org/wiki/Bipartite_graph separated into two sets of vertices that are not connected. Two colorable. Tree’s are bartite. Even cycle graphs Konig’s theorem - minimum vertex cover = maximum edge cover

https://en.wikipedia.org/wiki/Planar_graph https://en.wikipedia.org/wiki/Circle_packing_theorem

https://en.wikipedia.org/wiki/Intersection_graph all graphs are intersection graphs. Intersections of sets

https://en.wikipedia.org/wiki/Interval_graph intersection graph of a set of intervals

https://en.wikipedia.org/wiki/Comparability_graph things that are comparable in a partial order have an edge. Total order has complete comparaibility graph. Comparability graphs are perfect

cayley graph https://en.wikipedia.org/wiki/Cayley_graph turn group into graph. edges are generators. Can easily get infinite graph in this way

Software

networkx

graphtools igraph

hypernetx

boost graph Lemon

https://docs.rs/petgraph/latest/petgraph/ petgraph rust https://depth-first.com/articles/2020/02/03/graphs-in-rust-an-introduction-to-petgraph/

// cargo-deps: petgraph
use petgraph::prelude::Graph;
use petgraph::dot::Dot;

fn main() {
    let mut graph = Graph::<&str, u32>::new();
    let origin = graph.add_node("Denver");
    let destination_1 = graph.add_node("San Diego");
    let destination_2 = graph.add_node("New York");

    graph.extend_with_edges(&[
        (origin, destination_1, 250),
        (origin, destination_2, 1099)
    ]);

    println!("{}", Dot::new(&graph));
}

Representation

Set of pairs Adjacency list. multigraph

raw pointery. Ironically, graphs are easy to define in C. Raw access to pointers makes traversing around in the grap possible. Global questions/search about the graph become annying.

E,V,s,t. Functional rep. You see this in categorical presentations. This is a finite category and then a functor takes it to data. Multigraph really.

-- https://proofassistants.stackexchange.com/questions/1698/making-a-finite-graph-type-in-lean-introduction-rule
structure Graph where -- a choice. Make E V parameters or not.
    E : Type
    V : Type
    s : E -> V
    t : E -> V
-- It's not good data though. We're not going to be able to compute
def ex := Graph.mk Unit Unit (fun _ => ()) (fun _ => ())
def ex2 := Graph.mk Bool Unit (fun _ => ()) (fun _ => ()) -- two edges to one vertex


def Graph2 (V : Type) : Type := V -> V -> Prop

inductive ex1 : Bool -> Bool -> Prop where
    true_edge : ex1 true true

def ex2 x y := match x, y with
 | true, true => True
 | _,_ => False
def Set (X : Type) : Type := X -> Prop
-- a set of edges
def Graph3 (V : Type) : Type := Set (Prod V V)
--#print (<->)
-- #check Iso
-- theorem iso (V : Type) : Iso (Graph2 V) (Graph3 V) := (fun p => fun (x,y) => p x y, fun p => fun x y => p (x, y))

structure SymGraph (V) where
    g : Graph2 V
    sym : forall x y, g x y -> g y x



def main : IO Unit := pure ()

half edge

Topological Graph Theory / Planar

https://en.wikipedia.org/wiki/Planar_graph https://en.wikipedia.org/wiki/Book_embedding https://en.wikipedia.org/wiki/Topological_graph_theory

https://en.wikipedia.org/wiki/User:David_Eppstein/Graph_Drawing graph drawing.

Kuratowski’s theorem

Minors

https://en.wikipedia.org/wiki/Graph_minor - minors are formed from graphs via edge contraction, vertex and edge deletion

https://en.wikipedia.org/wiki/Forbidden_graph_characterization classes of graphs are often characterized by forbidden minors

https://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theorem - Robertson Seymour. Graphs, ordered by the minor relationship, form a well quasi-order

Extremal Graph Theory

https://en.wikipedia.org/wiki/Extremal_graph_theory graphons Szemerédi regularity lemma

Probablistic Graph Theory

https://en.wikipedia.org/wiki/Random_graph

Erdős–Rényi model

https://en.wikipedia.org/wiki/Percolation_theory

Algebraic Graph theory

Graph expanders

https://en.wikipedia.org/wiki/Adjacency_matrix https://en.wikipedia.org/wiki/Spectral_graph_theory cheeger constant. cheeger inequality

Positive and negative value on eigenvectors are a way of labelling or cutting graph.

https://en.wikipedia.org/wiki/Expander_graph sparse graph with strong connectivity properties. hard to cut apart.

Miracles of algerbaic graph theory

kepner and gilbert - graphs in language of linear algebra

Cut

https://en.wikipedia.org/wiki/Cut_(graph_theory) a

https://en.wikipedia.org/wiki/Bridge_(graph_theory) an edge who’s removal increases number of connected components Tarjan bridge finding algo Chain decomposition

https://en.wikipedia.org/wiki/Vertex_separator#Minimal_separators A set of veriies to separate graph in two

SDP Max cut approximation

Sherali Adams

Flow

https://en.wikipedia.org/wiki/Flow_network

https://en.wikipedia.org/wiki/Maximum_flow_problem

max flow min cut

Max cut

Decomposition

https://en.wikipedia.org/wiki/Modular_decomposition https://en.wikipedia.org/wiki/Split_(graph_theory) split decomposition https://en.wikipedia.org/wiki/Branch-decomposition

Tree Decompositions

https://en.wikipedia.org/wiki/Tree_decomposition There was also the kleene algebra variation of Treewidth is the width of a minimal tree decomposition Cops and Robbers pursuit evasion Elimination ordering https://en.wikipedia.org/wiki/Junction_tree_algorithm graphical models have their own terminology for this https://pacechallenge.org/past/ PACE challenge. Herusitics and exact Correspondence between Multilevel Graph Partitions and Tree Decompositions Parametrized algorithms Treewidth, pathwidth and cospan decompositions with applications to graph-accepting tree automata

Use the sql plan?

Encoding Treewidth into SAT SAT approach to cique width

Graph Partition

https://en.wikipedia.org/wiki/Graph_partition

Kernighan–Lin algorithm Huh. The opposite ordering of names to the TSP heurisitc. Take vertices with maximum improvement, swap them. Lock them?

https://en.wikipedia.org/wiki/Fiduccia%E2%80%93Mattheyses_algorithm Fiduccia–Mattheyses algorithm FM algorithm. terative partition

METIS hMetis for hypergraphs

Demmel Notes

Fiedler. split nodes into positive and negative of first eigenvector. +-1 Indicator vector. The cost is Sum (v_i - v_j)^2. Relax from boolean indicator. Graph Laplacian sLs. Balanced cut constraints sum s = 0.

https://web.eecs.umich.edu/~imarkov/pubs/book/part_survey.pdf huh using to reorder bdd hypergraph partitioning High-Quality Multilevel Hypergraph Partitioning KaHyPar https://github.com/kahypar/kahypar https://github.com/lnis-uofu/LSOracle lsoracle. uses kayhyper Graph partitioning is useful in logic synthesis?

parttion of sparse matrices search in a graph can be represented using multiplying by adjacency matrix

It’s almost “dual” to graph coloring, negating the sign of color color surafce. We want to clump colors as much as possible rather than

% functional
{color(N, C) : colors(C)} = 1 :- nodes(N).

#minimize {  edge(X,Y), color(X,C1), color(Y,C2), C1 != C2 } + 

% maximize the colors that are touching
#maximize {  edge(X,Y), color(X,C), color(Y,C)}

Optmization metrics: number of cut edges normalized in some way. “Volume” is sum of edges. ormalize by volume? Qutient, normalized cut

Karger’s algorithm - random for min cut. Randomly contract edges until you have only two vertices left. The edges between those are your guess for a cut and the set of contracted together vertcies are the two sides of the cut

Logic

https://en.wikipedia.org/wiki/Logic_of_graphs

model checking First order logic can ask about subgraph isomorphism. This is

Monadic second order logic. Existential second of logic let’s you talk about selection sets of certaain kinds. Model checking these formulas requires solving dificult NP problems. Many of the problems below fall into this class.

Courcelle’s theorem

MSO1 sets of vertices. cliquewidth graph

MSO2 sets of edges and vertices. treewidth

Problems

PACE https://pacechallenge.org/past/ https://www.optil.io/optilion/problems some kind of kaggle for optimuizatin problems https://sullivan.cs.utah.edu/#!/software

  • Twinwidth - minimum contraction sequence to single vertex SAT encoding
  • directed feedback vertex set - remove vertices to make graph acyclic
  • cluster editting - set of edge modifications (addition or deletion) of minimum size that transformsG into a cluster graph.
  • treedepth
  • treewidth
  • hypertree width
  • steiner tree

https://en.wikipedia.org/wiki/User:David_Eppstein/Graph_Algorithms https://github.com/ArrogantGao/TreeWidthSolver.jl

Easy

Topological sort reachability shortest path minimum spanning tree max flow min cut . A corolary on linear duality.

Many (all?) of the easy problems are reducible simply to a linear program.

https://en.wikipedia.org/wiki/Lexicographic_breadth-first_search Orders the vertices

Enumeration

https://en.wikipedia.org/wiki/BEST_theorem

Hamiltonian cycles

https://en.wikipedia.org/wiki/Hamiltonian_path Visit each vertex once. Travellign salesman problem is weighted relative

https://en.wikipedia.org/wiki/Eulerian_path visit every edge exactly once

Clique

https://en.wikipedia.org/wiki/Clique_problem Find maximal completely connected cluster (clique)

Ramsey theory guarantees clique exists

What Maximum Clique Algorithms Can Teach Us, And Vice-Versa

Coloring

https://en.wikipedia.org/wiki/Graph_coloring Register allocation

https://en.wikipedia.org/wiki/Edge_coloring chormatic index = minimum number of edge colors https://en.wikipedia.org/wiki/Vizing%27s_theorem every graph can be edge colored with close to the maximum degree (edge count on single vertex)

Covering

https://en.wikipedia.org/wiki/Covering_problems

Isomorphism

nauty bliss saucy

graph canonicalization. Find a way to sort vertices? If they all had unique attributes, sweet. https://en.wikipedia.org/wiki/Graph_canonization

Then number of neighbors, other little facts. properties of neigbors Could use properties of nehigbors Could use labelling of neighbors too. That becomes a self consistent search. However, if you already know certain orderings (based on properties). Or you could branch I’m not sure I’m understanding this the same way nauty does.

Graph hashing

https://github.com/calebh/dihash merkle tree version into a tree width version. Can a canonical (minimal) identifier be found via dynamc programming?

disjoint set partition data structure?

isomorphism vs bisimulation. Different but related ideas.

automorphism - permutation of graph such that is an isomorphism vertex orbit

Practical graph isomorphism II

Colorings are partitions. A mapping from vertices to numbers. Refinement

Logic Programming with Graph Automorphism: Integrating naut with Prolog (Tool Description)

import pynauty

g = pynauty.Graph(10)
print(g)

Interning alpha equiv terms graphlog. graphs as datalog objects. Graphs as the fundamental store. automorphisms + group union find

AC terms are unstructure graphs Typically terms are structured graphs.

(1,(2,3))

def graph_from_term(t):
    tid = fresh()
    graph.add_vertex(tid)
    if isinstance(t,set):
        # for set or multiset we don't want the indirection

    for n,c in enumerate(t):
        graph.add_vertex(n) # add intermiedate node lbaelling which child. Or if we can edge label do that
        graph.add_edge(tid,n)
        cid = graph_from_vertex(c)
        graph.add_vertex(n,cid)
    return tid


import networkx as nx
import matplotlib.pyplot as plt
def fun(name):
    def res(*args):
        G = nx.Graph()
        G.add_node(0)
        for arg in args:
            G = nx.disjoint_union(G,arg)
            G.add_edge(0,len(G) - len(arg))
        return G
    return res

def const(a):
    G = nx.Graph()
    G.add_node((0,a))
    return G
a = const("a")

plus = fun("+")
paa = plus(a,a)
G = plus(paa,paa)


nx.draw(G, with_labels=True)
#plt.show()


table = {}
def intern(G):
    h = nx.weisfeiler_lehman_graph_hash(G) # we should obviously cache this, but whatever
    matches = table.get(h) 
    if matches == None:
        table[h] = [G]
        return G
    else:
        if G in matches:
            print("found")
            return G
        for m in matches:
            #if m is G: # fast shortcutting
            #    return m
            #else:
            if nx.is_isomorphic(m,G):
                    print("iso")
                    return m
        matches.append(G)
        return G

a0 = intern(a)
print(table)
a = const("a")
a1 = intern(a)
print(table)
print(a1 is a0)



table = {} # enumerating in toplogica order would be nice. OrderedDict. We seem to be fine though. default dict guarantees this?
class Node():
    def __init__(self,id, term):
        self.id = id # use id(Node) ?
        self.term = term
    def __hash__(self):
        return hash(self.id)
    def __eq__(self,b):
        return self is b #self.id == b.id ?
    def __repr__(self):
        return repr(self.term)
def hashcons(x):
    # x is hashable and equality.
    s = table.get(x)
    if s != None:
        return s
    else:
        n = Node(len(table), x)
        table[x] = n
        return n

def hashset(iter):
    s = frozenset(iter)
    return hashcons(s)

def reify(): # reify returns the set of all things we've seen so far. Well-founded. We could have tracked them.
    return hashset(table.values())
# reify is transitively closed

empty = hashset([])
one = reify()
two = reify()
three = reify()
print(three)
three2 = hashset([two, one, empty])
print(three2 is three)
print(three2.id)
print(three.id)
print(three2)
print(three)


def pair(a,b):
    return hashset([hashset([a]), hashset([a,b])])

print(pair("a","b"))
print(pair("a","b") is pair("a","b"))

def union(a,b):
    return hashset(a.term | b.term)

def trans(s):
    if isinstance(s.term, set):
        set(trans(x) for x in s.term)
        return 
    else:
        return s

Hmm. this is also basically a method for tree isomorphism. More or less follows the lins of the ahu algorithm.

Hash consing generates ids that witness the well foundedness. hashunconsing

A unique id, but then we also kind of want to go back from id to terms. We could maintaini an id table, but from whence do we receive id?

Our memoizing table choices

  • Int -> Term

Hash consing does maximal compression to unique CSE form. To hash cons already built stuff is to perform congruence closure? disjoint sets of tid.


add(1,2,3).
add(1,2,4).
add(3,4,5).

root(Z,Z1) :- add(X,Y,Z), add(X1,Y1,Z1), root(X1,Xr), root(X,Xr), root(Y,Y2), root(Y1, Yr).

Hash consing is not appropriate for context dependency. The sharing is not dignified. Bisimulation as equivalence algebraic equivalence graph equivalence

AC shuffling. Terms equal modulo AC. Terms equal modulo AC and Alpha. That’s kind of cool.

query automorphisms - permutation symmettries of a conjunctive query.

query containment / query equivalence

Queries as ported hypergraphs. Chandra and Merlin. Bonchi says https://www.irif.fr/~greta/event/jul2nd2021-bonchi/

from z3 import *
S = Sort("S")
x, y, z = Consts("x y z", S)
R = Function("R", S,S,BoolSort())
Q1 = And(R(x,y), R()  )
Implies()

import networkx as nx

class HyperGraph(nx.Graph):
    counter = 0
    def add_node(i, attrs):
        attrs[""] = "node"
        super.add_node(i, )
    def add_hyperedge(*nodes):
        self.counter += 1
        attr["type"] = "hyperedge"
        super.add_node(counter, attr)
        for n in nodes
            super.add_edge(self.counter , n)    

class Var():
    def __init__(self, x):
        self.x = x

class Query(HyperGraph):
    #def var(x):
    # actually since it adds not seen nodes anyhow, don't bother
    #    self.add_node(x)
    #    return Var(x)
    def relation(name):
        def res(*args):
            self.add_node(name) # hyperedge modelled as 
            for i in args:
                if isinstance(i,Var):
                    self.add_edge( , , )




h(X,Y)

Uniqueness is kind of easier to enforce than maximal sharing (?) because subgraph identity is tough. One incoming edge. Forbid subgraph automorphisms? Can that be done? A minimal (labeled/colored) graph that you have a homomorphism to. Does this minimal graph have automorphisms?

Approximate matching. Convex relaxation Quadratic assignement problem On convex relaxation of graph isomorphism MILP A permutation matrix = 0-1 matrix with all
$PBP^T = A$ doubly stochastic matrix

https://en.wikipedia.org/wiki/Graph_homomorphism generalization of coloring. colorings are homomoprhisms to complete graph

Weisfeiler and Leman Test. https://davidbieber.com/post/2019-05-10-weisfeiler-lehman-isomorphism-test/ An iterative thing. Get a bunch of fingerprints. Actually looks a lot like partition refinement for autmata minimization. I suppose taking a graph, reducing to a canonical automata is a reasonable canonical object.

A SHORT TUTORIAL ON THE WEISFEILER-LEHMAN TEST AND ITS VARIANTS


for n in G.neighbors():
    hash((selfid,frozenset( G.neighbors ))) # multiset is better.

Eigenvalues of graph laplacian are a fingerprint. Automorphisms ought to show up in representation theory stuff somehow?

subgraph isomorphgism

https://en.wikipedia.org/wiki/Subgraph_isomorphism_problem

subgraph matching and query containment. You can use SQL to build a pattern that matches against a database. This is part of a general framework of homomorphisms.

CREATE TABLE k3(a,b);
INSERT INTO k3 VALUES (1,2), (2,3), (3,1);
INSERT INTO k3 SELECT k3.b, k3.a FROM k3;
SELECT * FROM k3;

-- automorphisms
SELECT e1.a, e1.b, e2.a, e2.b, e3 FROM k3 as e1, k3 as e2, k3 as e3 WHERE e1.b = e2.a and e2.b = e3.a and e3.b = e1.a;

Analysis of Graph Transformation Systems: Native vs Translation-based Techniques https://nicolasbehr.gitlab.io/ReSMT/#f1

https://en.wikipedia.org/wiki/Induced_subgraph induced subgraph. Subset of vertices + all internally connected edges.

neural subgraph matching subgraph mining

Graph Neural Network

Stanford CS224W: Machine Learning with Graphs

the power of graph learning - simons https://www.youtube.com/watch?v=iAxrFW1ku4I

Graph Rewriting / Graph Transformation

“Graph grammars”

See term rewriting drags term graphs

graph transformation Greta Graph TRansformation Theory and Applications (GReTA) internationa http://graph-transformation-for-software-engineers.org/ https://www.irif.fr/~greta/ Graph Transformation for Software Engineer He’s been givng tutorials

ICGT international conference on graph transformations double pushout. A pattern L. the “kept” bits K the right hand side R, glued in

A Software Package for Chemically Inspired Graph Transformation https://jakobandersen.github.io/mod/ Why did they name it this. Hmm. reaction enumeration. Chemical reaction modelling. That’s intriguing.

AGG GP 2 https://github.com/UoYCS-plasma/GP2

GGL https://www.tbi.univie.ac.at/software/GGL/ graph grammar obrary. Built on bosot graphs GDGEN.Net PORGY https://www.youtube.com/watch?v=D_YHlXawg9o&ab_channel=GReTASeminar

GRAPE verigraph https://link.springer.com/chapter/10.1007/978-3-319-75396-6_9

galoisenne Lots of cool links

https://github.com/AlgebraicJulia/AlgebraicRewriting.jl catlab. C-Set rewriting. https://arxiv.org/abs/2111.03784 Computational category-theoretic rewriting. A generalization of graph rewriting? Typed graphs.

Table 1 AGG[34] Y N S N 2017 Y N Both Groove[27] Y N S N 2021 Y N App Kappa[14] N N N 2021 Y Y App VeriGraph[1] Y N D Y 2017 N Y Lib ReGraph[13]

Chemical rewriting “Chemical Graph Transformation and Applications” https://www.youtube.com/watch?v=mzIXfsp-eJE&ab_channel=GReTASeminar SMILES is a graph. chemical databases. See note on chemistry

My temptation would be to: find a pattern L (using datalog/sql probably), store result in an env dict, blow it all away, paste in R filling in from the env.

The “env” can be represented as a graph homomorphism though from the pattern (a dictionary mapping vertices to vertices and edges to edges).

CHR

CHYP replacement

wacksmackadoo wofram hypergraph rewriting https://www.wolframphysics.org/

import sqlite3
import networkx as nx

def query_of_graph(G):
    counter = 0
    froms = []
    wheres = []
    for (i,j) in G.edges:
        e = f"e_{i}_{j}"
        froms.append(f"edge AS {e}")
        wheres.append(f"{e}.i = {i}")
        wheres.append(f"{e}.j = {j}")
    froms = ",".join(froms)
    wheres = "AND".join(wheres)
    return f"FROM {froms} WHERE {wheres}"

def db_of_graph(G):
    db.execute("INSERT INTO verts VALUE (?)", G)
    db.execute("INSERT INTO edge VALUES (?,?)", G.edges)
    db.execute("INSERT INTO attrs VALUES (?,?)", [])




import networkx as nx
G= nx.Graph()
G.add_node(1, foo=7)
print(type(G.nodes[1]))
print([type(n) for n in G.nodes])

import sqlite3
import networkx as nx
def db_of_graph(conn, G):
    con.executemany("INSERT INTO nodes VALUES (?)", map(lambda v : (v,),  G.nodes))
    con.executemany("INSERT INTO edges VALUES (?, ?)", G.edges)
def graph_of_db(con):
    G = nx.DiGraph()
    res = con.execute("SELECT * FROM nodes")
    G.add_nodes_from(map(lambda x: x[0], res.fetchall()))
    res = con.execute("SELECT * FROM edges")
    G.add_edges_from(res.fetchall())
    return G
def query_of_graph(G):
    selects = []
    froms = []
    wheres = []
    for node in G:
        froms += [f"nodes AS v{node}"]
        selects += [f"v{node}.v AS v{node}"]
    for i, (a,b) in enumerate(G.edges):
        froms += [f"edges as e{i}"]
        wheres += [f"e{i}.src = v{a}.v"  , f"e{i}.dst = v{b}.v"]
    sql = "SELECT " + ", ".join(selects) + \
          "\nFROM " +  ", ".join(froms) + \
          "\nWHERE " + " AND ".join(wheres)
    return sql
G = nx.path_graph(7, create_using=nx.DiGraph)
lhs = nx.path_graph(3, create_using=nx.DiGraph)
con = sqlite3.connect(":memory:")

con.execute("CREATE TABLE nodes(v)")
con.execute("CREATE TABLE edges(src,dst)")
db_of_graph(con, G)
res = con.execute(query_of_graph(lhs))
print(res.fetchall())
# Result: [(0, 1, 2), (1, 2, 3), (2, 3, 4), (3, 4, 5), (4, 5, 6)]

print(graph_of_db(con))
"DELETE FROM nodes WHERE nodes.v = ?"
"DELETE FROM edges where edges.src = ? OR edges.dst = ?"

con.execute("DELETE FROM nodes")
con.execute("DELETE FROM edges")
colors = nx.complete_graph(2) # a two coloring
db_of_graph(con,colors)
# symmetrize. Maybe db_of_graph should do this. if not isinstanc(G,nx.DiGraph)
con.execute("INSERT INTO edges SELECT edges.dst, edges.src FROM edges")

res = con.execute("SELECT * FROM edges")
res = print(res.fetchall())
res = con.execute(query_of_graph(G))
print(res.fetchall())
# [(1, 0, 1, 0, 1, 0, 1), (0, 1, 0, 1, 0, 1, 0)]

examples:

import networkx as nx

G = nx.Graph()
G.add_edges_from([
    (1,2),
    (2,3)
])

class Rule():
    def __init__(lhs,rhs,iterface):
        self.lhs = nx.Graph()
        self.lhs.add_edges_from(lhs)
        self.rhs = nx.Graph()
        self.rhs.add_edges_from(rhs)

class TreeRule(Rule):
    def __init__(self):


def run_rule(G, rule):
    match = nx.subgraph_match(rule.lhs, G)
    delete(G, match)
    return apply(G, rule.rhs)




morph(id,X,Y), morph(F,Y,Z) ==> morph(F,X,Z).
morph(swap, ...) %hmm.


graphize(id, X,Y) :- morph(id,X,Y).
graphize(comp(F,G), X, Z) :- %gensym(Y), 
                      graphize(F,X,Y), graphize(G,Y,Z).
graphize(otimes(F,G), [X,Y], [Z,W]) :- graphize()


graphize(id,X,X).
graphize(comp(F,G), X,Z) :- graphize(F,X,Y), graphize(G,Y,Z).
graphize(otimes(F,G), X-Y, Z-W) :- graphize(F,X-A, Z-B), graphize(G, A-Y,B-W). % difference lists. or append(X1,X2,X), 
graphize(swap, [A,B|Z]-Z, [B,A|Z]-Z).

% inverse collection out of chr
morph(F,A,B) \ collect(F,A,B)  ==> true.
collect(F,A,B), collect(G,B,C) ==> collect(comp(F,G),A,C).


auto :- autochr, deauto.

autochr

prove :- auto, rw(foo), simp, .


main() :- theorem(forall(X,foo(X)),
          (auto, simp, rw, )            
) 
vs
theorem(forall(X,foo(X))),
auto, simp, qed,

theorem(myname, forall(X,foo(X))).
auto. simp. qed.

% axiom
asserta(theorem(forall(X,foo(X)))).

axiom(F) :- asserta(theorem(forall)X,foo(X)).

Pfaffian orientation

https://en.wikipedia.org/wiki/Pfaffian_orientation A directon to each edge such that each cycle https://tex.stackexchange.com/questions/692892/kasteleyn-orientation-for-square-lattice

Kastelyn orietnation

FKT algorithm for counting perfect matchings. Katelyn Temperley Fisher. Dimers. pfaffian of skew symmettric matrix can be reduced to determinant counting is useful in stat phys. entropy. https://en.wikipedia.org/wiki/Geometrical_frustration https://en.wikipedia.org/wiki/Holographic_algorithm

Matchings

https://en.wikipedia.org/wiki/Matching_(graph_theory) a set of edges such that none share vertices

maximum matching

https://en.wikipedia.org/wiki/Perfect_matching pick edges such that exactly one edge touches every vertex

Related to https://en.wikipedia.org/wiki/Edge_cover where each vertex must touch at least one edge

Infinite Graphs

https://en.wikipedia.org/wiki/End_(graph_theory)

Compactness

Misc

https://en.wikipedia.org/wiki/Graph_polynomial Tutte polynomial

bipartite graphs