Graph Theory
The goal of this project was to develop a computer program for detecting symmetries in vertex-colored undirected graphs. The program should mimic the algorithms in the saucy
symmetry detection system. The saucy page
was consulted for papers that describe how saucy
works and give worked-out examples tracing the execution of the saucy
algorithm. In what follows we will call the program saucy_clone
.
One source of intractability in SAT is the presence of structural symmetries in the solution space. In this context, a symmetry is a permutation of the literals of a CNF formula that leaves the formula unchanged. The symmetries of an -variable formula induce an equivalence partition on the formula’s possible truth assignments. The assignments in a given cell of such a partition are equivalent in the sense that the formula evaluates to the same truth value (either 0 or 1) on all of them. So rather than search in the space of the possible assignments, a SAT solver could be directed to search in the much smaller space of the equivalence partition. This approach is generally referred to as and it has many variants. In particular, symmetry breaking consists of the following steps:
This approach to symmetry breaking has led to dramatic pruning of the search space in some cases. In particular, it works extremely well for pigeon hole instances (unsatisfiable CNF formulas that encode placing pigeons in holes such that no hole has more than one pigeon). But in many cases the reduction in the size of the search space does not translate to a reduction in run time due to the overhead introduced by the SBPs.
In any case, this project is not about symmetry breaking for SAT. Rather, as often happens in research, the unexpected foray into symmetry detection in graphs led to the development of the saucy
program which differs in fundamental ways from earlier symmetry detectors and achieves an unprecedented six orders of magnitude performance edge.
Before embarking on this project it is highly advisable that you read the following references:
K. A. Sakallah, “Symmetry and Satisfiability,” in Handbook of Satisfiability. vol. 185, A. Biere, et al., Eds., ed: IOS Press, 2009, pp. 289-338. PDF
H. Katebi, K. A. Sakallah, and I. L. Markov, “Symmetry and Satisfiability: An Update,” in Thirteenth International Conference on Theory and Applications of Satisfiability Testing (SAT), Edinburgh, 2010, pp. 113- 127. PDF PPT
In addition, you should consult the saucy webpage
for additional references and links to related work.
The project is designed to have a sequence of well-defined deliverables that insure progress towards the final “product” which is a saucy
clone.
The vertices of an -vertex -color undirected graph are assumed to be numbered consecutively from to . The colors partition the vertex set into different cells such that vertices in any given cell share the same color. In addition, it is assumed that vertices of the same color are numbered consecutively with no gaps (see example below). A graph input file is a text file consisting of a header followed by a listing of the graph edges. All fields in the input file should be decimal integers. White spaces, including newlines, serve as field separators and are ignored. The file header for a graph that has vertices, edges, and colors has the following format:
where is the index of the least vertex in the cell corresponding to color . In what follows we will refer to as the color change locations. For example, the header
describes a graph with vertices, edges, and colors. The colors partition the set of vertices into the following three disjoint subsets: . The last two numbers in the header indicate that color starts at vertex whereas color starts at vertex ; they also implicitly indicate that color applies to all vertices numbered lower than . Note that when the list of color change locations is empty. Graph edges are specified as pairs of vertices given in either order (since the graph is undirected). Note also that the order of edges in the listing is unimportant. An example colored graph and its associated input file are shown in Figure 1.
A useful tool for drawing graphs is Graphviz
which can be downloaded from here. The input text format and graphical output format of Graphviz
for the graph of Figure 1 are shown in Figure 2.
Permutations are typically expressed in one of two ways: tabular form or . For example, given the set the permutation that maps to , to , and to can be expressed as the table
or as the cycle . Cycle notation is very compact when the number of vertices moved by a permutation is much smaller than . The output of saucy
is a set of (at most ) expressed in cycle notation. Generators are vertex permutations that, when combined in all possible ways, are guaranteed to yield all possible graph symmetries.
Within saucy
, the basic data structure for encoding permutations is the so-called (OPP) which is a generalization of tabular notation that allows for the implicit encoding of a set of permutations. This is detailed in here. The OPP data structure is key to the way that saucy
searches for symmetries in the permutation space whose size, for a graph with vertices, is .
Here are several example OPPs and the permutation sets they encode.
A lot of what saucy
does involves the manipulation of ordered partitions (OPs), primarily refining (i.e. splitting) cells by changing the positions of the affected vertices. To do this efficiently, saucy
uses a to store the vertices of the OP along with three other “helper” arrays to keep track of cell boundaries and lengths:
To enhance readability, the names used here are not the same as in the
saucy
source code
As an example, the OP
is encoded as:
Strictly speaking the Position array is not needed as it is just the “inverse” of the Vertex array, but it does speed up OP processing. The slightly mis-named CellLength array is defined as described above so that singleton cells can be identified quickly by checking if their corresponding entry in CellLength is 0. In addition, CellLength is defined only at the positions corresponding to cell fronts.
As an example of using this data structure, given a vertex , its position in the OP is , its cell starts at position , and the size of the cell is .
The goal of this deliverable is to write a parser for the text format for encoding colored graphs described in Section 2. This parser should do the following:
Graphviz
format and run it through Graphviz
to draw itFor extra bonus, the output may also contain statistics about the graph such as the color degree of each vertex (how many neighbors a vertex has of a certain color).
The goal of this deliverable is to implement the vertex partition refinement procedure which is the main mechanism for distinguishing non-symmetric vertices in the graph. Consider an ordered partition of the graph vertices and let be the of vertex with respect to cell of the partition. Specifically, is the number of vertices in cell Wi that are adjacent to v (i.e., the number of connections v has to cell Wi). An ordered partition is if all vertices in each cell of the partition have the same color-relative vertex degree. Partition refinement is triggered if the partition is not equitable, meaning that a vertex in some cell of the partition has a color-relative degree that is different from the color-relative degrees of the rest of the vertices in that cell. That vertex can, thus, be distinguished by separating it from the other vertices in the cell to obtain a partition (i.e., one that is obtained by splitting some of its parent partition cells). The resulting partition may still be inequitable, triggering another round of splitting. This process continues until an equitable partition is obtained.
The core operation in partition refinement is the (potential) splitting of a cell by an inducing cell . This is done by computing the degrees of ’s vertices relative to and creating a partition of such that each of its cells has vertices with the same degree relative to . This operation, which we will call refine_cell
, takes the current partition along with the target and inducing cells, and returns a (potentially) partition and a (potentially empty) list of “new” cells that form a partition of :
The refinement procedure can now be implemented by maintaining a queue of inducing cells which are processed one at a time by refine_cell
. If this causes a target cell to be split, its parts are inserted in the queue for later processing. Given an initial queue of inducing cells, the pseudo code for partition refinement is roughly as follows:
00 refine (OP P) {
01 while not empty(Q) {
02 I = pop(Q);
03 for each cell T with connections to I {
04 (OP P, Cell List L) = refine_cell(OP P, cell T, cell I);
05 if not empty(L) {
06 if T is in Q, remove it;
07 for each cell t in L
08 push(t, Q);
09 }
10 }
11 }
12 }
Note that there are many optimizations that can make this procedure more efficient. In particular, saucy
maintains a separate queue of singleton inducing cells and processes that queue before it processes the queue of non-singleton cells. In addition, saucy
eliminates the step of removing from the queue a target cell that also happens to be an inducing cell (line 06). This does not affect the correctness of the procedure: if refinement splits cell into, say and , the queue will now contain two copies of (assuming it is the left cell) since no longer exists! Having duplicate copies of refining cells in the queue causes no harm other than repeating the connectivity checks to other target cells. For very large sparse graphs such checks are much less expensive than locating and removing a cell from the queue.
An example of partition refinement is shown in Figure 3. The initial unit partition in is refined to the 2-cell partition in based on vertex degrees. The two cells of partition are then inserted into , the inducing cell queue. The cell at the top of the queue, , is now popped and used to refine the target cell . Since the number of connections of vertices 0 and 6 to the inducing cell are equal, cell cannot be refined. The next inducing cell at the top of the queue is , and when used to refine target cell , it splits it into two cells, and , yielding partition . Continuing in this fashion, the algorithm terminates after a few more steps producing the final equitable partition .
The implementation of partition refinement in saucy
includes several optimizations that help to reduce its computational complexity. For example, singleton cells need not be “touched” during refinement since they cannot be split. In addition, saucy
applies partition refinement to both the top and bottom partitions of an OPP.
For this deliverable, we wrote a partition refiner that does the following:
The goal of this deliverable is to construct the left-most branch of the permutation search tree. This branch is referred to as subgroup decomposition. Starting at the root of the tree and at subsequent levels, involves the following steps:
The queue actually contains the cell fronts of cells, and so will have a duplicate cell front.
An example of subgroup decomposition is shown in Figure 4. The OPP at the root of the search tree corresponds to (an uncolored version of) the graph of Figure 1. It consists of two cells obtained by separating the graph vertices based on their degree. The first in this decomposition is to map vertex to itself which yields an OPP that is not equitable. This triggers two refinement iterations that result in splitting the only non-singleton cell in the OPP into three cells, separating vertices and , and then from the other vertices. The second decision maps vertex 5 to itself but does not trigger further refinement. Similarly, the last two decisions map 0 to itself and 1 to itself yielding the final discrete OPP that corresponds to the identity permutation.
For this deliverable, we wrote a subgroup decomposition program that does the following:
To complete the cloning of saucy
, we had to construct and traverse a permutation search tree. The first part of the tree is the left-most subgroup decomposition path we developed in deliverable III. Each node along that path encodes a subgroup , i.e., a subgroup that “fixes” the vertex chosen at that level. To complete the tree, the other possible mappings of that vertex must be explored and each such mapping can lead to a subtree in the search space that may or may not contain valid symmetries. Under each such mapping, the search must continue until a permutation that pre- serves the graph edge relation is found, or until it can be shown that no such permutation exists. The full details of this search algorithm can be found in here which should be reviewed carefully before embarking on the implementation.
For this deliverable we wrote a program called saucy_clone
which includes the following modules:
saucy_clone
was tested on a set of graphs and its results compared to those produced by saucy
.
Love,
Ahmed Jazzar