6/25/2012 Update

During our meeting last week we discussed ways in which we could refine our visualization. We tried to come up with several usage scenarios to guide our progress and make the tool more useful.  We plan to look at different aspects of the algorithm and try to implement a way in which our tool can demonstrate each part.  Dr. Dwyer suggested coming up with questions that we had when we first learned to algorithm then altering the tool to answer these questions.  This will help us keep sight of our goal to produce a helpful learning tool and give us a better guide to reach our goal. 

Additionally, Elena and Dr. Dwyer expressed interested in making the tool more user friendly.  Dr. Dwyer suggested that instead of having a combo box for every node we should consider having a static position for the combo box.  Instead of having to click several times to view information about a node, Dr. Dwyer suggested selecting a “mode” using the combo box and hovering over each node to retrieve the information.  This saves the user several clicks in order to get the same information. In addition to Dr. Dwyer’s suggestion, Elena recommended having pause/play buttons to build the graph instead of having to user the slider or clicking the right arrow to build.  This makes it much easier to see the graph being built incrementally.  Over these last couple days, I have implemented both of these features and cleaned up the flash builder code.

Finally, we discussed removing some of the clutter on the visualization.  Right now the user can select “Unsat Clauses” mode and view ALL of the unsat clauses in the text box on the side of the page.  This information is not very useful to someone learning the algorithm and can become very overwhelming.  The original intent for displaying all of the unsat clauses was to show how the amount of unsat clauses changes throughout the algorithm. We decided that it would be much easier to visualize the change in unsat clauses graphically and discussed the possibility of having a sort of timeline. We are currently looking at tools that we can use to display the timeline and graph.  Hopefully next week we will have made a decision regarding the timeline and can continue progress.

-Mary

Project Updates 6/18

At our weekly meeting last Thursday, Dr. Dwyer provided very helpful feedback on the current state of our visualization.  Some of his suggestions included adding a key at the bottom of the page and having a static location for the drop down box.  Having the drop down box in one place will allow the user to select a certain "mode" (conflict clause mode, propagations mode, or unsat clauses mode) then hover over the nodes to view the specific information.  Rather than having to select a new mode every time the user hovers over a node, the user can see how the information selected in the mode changes with each node by simply selecting a mode and hovering over other nodes.  This will make the visualization more user friendly.

As I mentioned last week, Maggie and I decided to split the work.  For the time being she will be working (and updating the blog) on the FlashBuilder portion and I will be working on the MiniSAT side.  So far, I have altered the MiniSAT code further to allow output of nodes involved in a conflict clause.  Previously in one of our meetings we discussing the possibility of having the nodes that led to a conflict light up when the user hovered over the conflict node.  The change I made to the MiniSAT code will allow Maggie implement this feature.

-Mary

June 11, 2012

We have finished refactoring the code and have put both the MiniSAT code and the FlashBuilder visualization code into an SVN so we can work simultaneously. The plan is for one of us to work on the MiniSAT code while the other is working on the Flashbuilder code.

Previously our visualization had a pop up text box for each node. This text box appeared the user hovered over the node with the mouse.  The text box displayed the propagations associated to that node and the conflict clause if the node was a dead end.  This text box looked very nice when there were a small amount of propagations, however if there were too many propagations it seemed to get a little cluttered. Early in May we discussed the possibility of adding a drop down menu when the the user hovers over the node as a fix for the clutter.

We implemented this feature this last week.  The drop down menu includes the following options: Propagation, Unsat Clauses, Conflict Clause. In a text box off to the side (the text box that previously showed the unsat clauses for a node when the graph was being built) the selection is shown.  Below is an example where the "Propogation" option was selected from the drop down box of node -14 (note that the graph is only partially built):

As shown above, the slider bar indicates the progress of the graph and can be used to add or remove nodes.

As with the slider bar and the scrollbar, the combobox has some issues getting and losing focus.  I will continue to work on this issue, although it may require us to look for a different library or toolset.

-Mary

June work

Last week we decided in a summer meeting schedule so we can be more consistent. We plan on meeting as an entire group every Thursday. In addition to these meeting times Maggie and I will likely meet on a regular basis to discuss progress via Skype or in person. This week we are working on refactoring both our flash builder code and our MiniSAT code. We would like to begin working on the same code base to expedite the progress. While it has been good experience creating our own code and seeing how our implementations differ, I think it will be very beneficial to work on the same code base. We will have to be more organized with dividing tasks but I think we will be able to cover more ground this way. Additionally, since we began by implementing tasks individually refactoring our code gives us the opportunity to combine ideas and take "the best of both". Mary

5/29

This last week I’ve worked on making the visualization more user friendly.  Previously I was having an issue with the scroll bar I added to the clauses textbox.  Since I had also attached the graph to a Pan Zoom Control, when I was scrolling the text box I was also moving the graph!  After a little reading and some trial and error the problem has been fixed.

We discussed in one of our earlier meetings the possibility of adding a slider bar to indicate how the progress of the graph.  The user can still build the graph using the left and right arrows, however if the graph is very large, building the graph can take a long time. These large graphs are the main reason we decided to implement the slider bar.  The user is now able to use the slider bar to build the graph.  This is a very nice feature that has been implemented; however it needs a little bit of work yet.  There is some difficulty getting focus on the slider bar when the program is first launched. I will continue working on this issue throughout the week. We have a scheduled meeting this upcoming Thursday to discuss what the final visualization will include (since the deadline is only about a month away) and begin designing the poster for the poster session at Grace Hopper 2012.

May Updates

We had our closing semester meeting during the first week of May.  During that meeting we delegated tasks which would be accomplished over the summer.  For the visualization, Maggie and I will add in the conflict clauses.  I have begun implementing this portion.  As of now, when a dead end is reached in the visualization if you hover over that node a box shows up alongside the node listing the propagations and the conflict clause added.   We also discussed the possibility of displaying the implication graph for each the dead ends.  I have not implanted that functionality yet but I hope to have that completed for the final demo.  At our meeting in early May we discussed adding a text box that shows all of the currently unsatisfied.  This feature will basically let the user visualize the impact of each assignment.  I currently have this implemented in my visualization.  I separated the unsatisfied original clauses from the unsatisfied learnt clauses.  At one point we also discussed have a text box for each node with statistics such as number of unsatisfied clauses, number of satisfied clauses, etc.   I will be discussing this with Dr. Dwyer at our meeting whether or not we want to implement this. 

In addition to the visualization, I have been continuing my reading for the conflict clause learning. 

Our visualization poster was accepted to the general poster session at Grace Hopper J, so we will begin authoring that probably within a week.

-Mary

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