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