4/17 Update

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

April 10, 2012

Recently, we have been working on implementing an interactive SAT visualization using Adobe Flash Builder and the Flex libraries. In the past several weeks, we studied Flash Builder demos and worked on isolating a tree structure. We then worked on making it possible to zoom in and out on different areas of the graph and worked on populating the nodes with data. We then worked on parsing data and using that data to construct the tree. Our current task is to parse the data output by the SAT solver and build an interactive tree representation of the search space. Our hope is that the tree will be able to represent decision levels, assumptions, conflict clauses, and backtracking.

On the theoretical side, we have been studying chapters 3, 4, and 9 of Decision Procedures by Daniel Kroening and Ofer Strichman. Our plan is to learn the theory behind SMT solvers, our next area of focus.

-Maggie

April 3, 2012

This week we are working more on the visualization of the MiniSAT solver. We are loading sample files and creating arrays based on the information in the files.  We are also continuing to discuss our approach on how to move forward with the visualization.  On my own project, I am continuing to read the research that has already been done in the area in order to get a better idea of how I should approach the project.