July 19, 2012

In addition to our work with the SAT visualization, we have been interested in modeling real problems as Boolean satisfiability problems, particularly Sudoku puzzles. I have been working on a script that takes as input a Sudoku puzzle represented as a string (a sequence of each square's value, from top-to-bottom and left-to-right), converts it to its representation in conjunctive normal form,  and outputs a CNF file readable by MiniSAT.

When represented as SAT problems, Sudoku puzzles are very large (729 literals), but not overly difficult to model.
Sudoku puzzles in SAT require clauses specifying that:
-Every square may only hold values from 1-9, and each square may only hold one value.
-Every value must exist in every row, but must exist only once in each row.
-Every value must exist in every column, but must exist only once in each column.
-Every value must exist in each 3x3 square, but each value may only appear once in that square.
-Each square holding a value at the beginning of the puzzle must be asserted.

There is a fairly elegant literal encoding for Sudoku that makes it much easier to interpret the results of the SAT solver. A square in Sudoku can be represented as p(i, j, n), where i is the row, j is the column, and n is the value assigned to that square. Thus, the clause 234 asserts that the square in the 2nd row and the 3rd column is assigned the value 4. Negation works similarly; -235 asserts that 5 cannot be assigned to the previous square.

I am looking forward to seeing how MiniSAT handles these SAT instances and discovering what can be learned from testing our system on a real problem.

-Maggie

Project Updates (7/19)

At our meeting last week we discussed further changes that should be made to the visualization.  First we decided on the statistics that should be included in the graph: size of the partial solution, number of open clauses (separated into learnt and original), and number of learnt clauses (this excludes the ones that have been forgotten).  We then discussed how the page should be organized and decided that the textbox, graph, and tree should all somehow be coordinated.  To coordinate the three structures, I implemented a couple new features.  When the user hovers over a node in the tree, the 4 corresponding nodes in the graph blink to indicate the location and the textbox displays the corresponding statistics. Previously there was a slider bar that indicated the progress along the tree, however I think it may be easier to navigate through the tree using the nodes on the graph.  Thus, I disabled the sliderbar (it is still visible and marks the location on the graph, but the user cannot use it to navigate through the tree) and am going to make the nodes on the graph buttons so the user can simply click on the node in the graph to build the tree.  In the upcoming week, I will also be redoing the dropdown box.  The drop down box will contain the same statistics found in the graph.  The user will have the option to view one or all of the statistics.  When the user makes his/her selection the graph will be updated to show one or all of the statistics and, when the user hovers over nodes in the tree, the corresponding statistic(s) will be shown in the text box.

-Mary

7/11 Vis Update

Over the two weeks we have been working on getting a prototype graph to navigate through the tree.  We found several examples on the web and decided to implement one that used flare.  Right now our graph shows the currently unsatisfied clauses at a particular node.  I implemented functionality to navigate through the graph using the scroll bar.  Also the current state of the tree is reflected in the graph by boldfacing the node in the graph corresponding to the most recently added node in the tree.  Over the next week I will be gathering more statistics MiniSAT and adding more lines to the graph.   Eventually, I would like to have check boxes alongside the graph listing the statistics so the user could select which ones he or she would like to view.  In addition to the graph, I will be implementing a legend for the tree to describe the colors of the nodes.

-Mary

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