Make documentation for formulas generated from graphs more specific

[jakobnordstrom]

A suggestion regarding documentation of formulas generated from graphs.

(1) Say that the formulas can be generated from graphs, and that general info about graph formats and families can be found at blah.

(2) Then, importantly, briefly specify the only graph families that are relevant for this family. Quick examples:

(a) For PHP we want only bipartite graphs, and for UNSAT instances we want graphs with more left-hand vertices than right-hand vertices (or at least wihout complete matchings). If there is a complete matching, the formula is SAT.

(b) For subset cardinality formulas we want bipartite graphs that are regular on both sides and have bounded, even degree. Add an extra edge to get an UNSAT instance.

(c) For Tseitin, only undirected graphs are relevant.

(d) For pebbling, only DAGs are relevant. (Do we allow multiple sinks, but the way? I guess there is no real reason not to.)

Et cetera...