This last week we spent time learning the Simplex Method as a part of our understanding of SMT. We looked at both the classical and general simplex methods.
On the visualization side, we modified our MiniSAT code to output a file which can be read by flashbuilder to produce a graph. We built and colored the graph based on this output file.
For example with a tab delimited output file we generated the following graph:
The labels in each node indicate the assumption made at each set of the SAT solver. The colors indicate if the assumption made at that node and the associated propagations participate in a solution (green), aren't part of the solution (grey) or correspond to the addition of a conflict clause and a dead end (red). The root node "r" simply indicates the root of the graph. Each of the graph levels corresponds to a decision level. For example the node "-1" corresponds to the decision level 0. Further, when the mouse hovers over a specific node, the propagations associated with that node's assumption are displayed in a textbox below the node. For example the assumption"19" has associated propagations -3,-7,-9,17,-14 as shown below:
On my own project, I am continuing to read the current reseach to get a better idea of how to approach the problem.
-Mary
No comments:
Post a Comment