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

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.

March 2012

Throughout March we have read chapters 3 and 4 in the book Decision Procedure and have been discussing the content in both our small and large group meetings to better understand the content.  Also, Maggie and I have been working with Elena on the visualization of the MiniSAT algorithm.  We decided to use Flash Builder and Flare for this visualization.  So far we have been going through the examples provided from the flare.prefuse.org website to get better idea of how to implement our visualization.  We figured out the zooming capability and have created our own trees using Flash Builder.  In addition to the SAT/CSP project, I have been working on my own project for conflict analysis in CSPs.  So far on this project I have created a variable ordering specifically for the zebra problem which selects one variable per cluster and jumps across clusters.  The purpose of this variable ordering is to study how CBJ identifies the constrains and creates the conflicts.  Additionally, I have implemented a piece in my code which takes a pre assignments and searches for a solution based on the partial assignment.  From here, I plan to read the relevant research which has already taken place regarding conflict analysis in CSP to build a better intuition of the material.

-Mary