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