It depends on what you are trying to model.

The following Alloy module has one command that gives a sequence of solutions, each of which has exactly on identified subgraph of size three.  By stepping through the solutions you will see every subgraph of size three.

If you want to check some fact about each subgraph, then you can do that, too: a pair of examples (one valid, one invalid) is given.  In this style you cannot check facts about combinations of subgraphs (the numbers will grow too fast to be practical).

module directed_graph

abstract sig Graph{node : set Node}

abstract sig Node{edge : set Node}
one sig n1, n2, n3, n4, n5, n6, n7  extends Node{}

fact edge{ // layout of graph
   edge = n1->n2
            +n1->n3
            +n2->n4
            +n4->n3
            +n3->n4
            +n4->n6
            +n3->n5
            +n5->n7
            +n7->n6
            +n7->n2
}

one sig Three_Graph extends Graph{} {#node = 3}

examples: run{} // see all three graphs, one at a time.

no_3_graph_has_all_edges: check{ // true of example above
   let n = Three_Graph.node | // nodes in selected sub-graph
      n<:edge:>n != edge
}

every_3_graph_has_exactky_two_edges: check{ // false of example above
   let n = Three_Graph.node | // nodes in selected sub-graph
      #(n<:edge:>n) = 2
}

--
Jeremy L. Jacob        Tel: +44-1904-43-2747    Fax: +44-1904-43-2767
Jeremy.Jacob@cs.york.ac.uk    http://www-users.cs.york.ac.uk/~jeremy/
Dept. of Computer Science, The University of York, YORK, YO10 5DD, UK

Thanks, Dr. Jacob.

It definitely gives me a very good start point.  I will work on this.

Best,

Jiangfan