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

February, 2012

This semester, we have been working on becoming familiar with SAT solvers and methods. In learning how SAT solvers work, we have begun to explore the parallels between SAT solvers and CSP solvers, which can be used to solve the same problems but use different modeling techniques and search methodologies.

In order to delve into SAT, we have been exploring a well-known solver called MiniSAT (http://minisat.se). In order to understand how MiniSAT works, we traced the functions of the program and printed out the assumption and trail at each decision level. In order to parse the MiniSAT code more effectively, we read a paper by Niklas Eén and Niklas Sörensson, the creators of MiniSAT. The paper, titled “An Extensible SAT-solver”, explains the basic functionalities of the solver’s classes and methods as well as an overview of its core algorithms. It has been immensely helpful in understanding how MiniSAT propagates, learns conflict clauses and traverses the search space.

Recently, we have been working on a visualization of the MiniSAT search process. Using the dot graphing language, we can program MiniSAT to output dot code to a file, with each assumption represented as a node in a tree, and with backtracking being represented as separate branches of the tree. This exercise is very rewarding in that it provides a simple graphical interpretation of SAT solving. Once able to output dot code during the program’s runtime, we are working on storing information relevant to outputting the graphs nodes and branches into data structures that we can then store in our modified MiniSAT code. 

--Maggie

Update

Sorry for the delay! Our group has been busy reading a paper describing the implementation of MiniSAT (http://minisat.se/downloads/MiniSat.pdf).  We've tried to carefully dissect this paper to understand the how it solves SAT problems.  So far we have made very good progress on this task and have a decent understanding of how it works. We have also adjusted the MiniSAT code so that it outputs a file that we can run on a dot renderer to produce a primitive graph.  We spent a lot of time designing the graph and each implemented our own sort of graph.  We presented our graphs to our advisers who gave us input on them.  We just implemented a data structure that holds the node information of the graph.  Our plan is to finish polishing up the graph and then move toward the animation. 

-Mary

Week 4 Update

During week four we tried to compile MiniSAT on our own laptops and tried to get started using and IDE (VisualStudio 2010 or Eclispe).  In the past I've found that using one of these IDE's dramatically decreases the time I spend debugging and programming in general.  However, I've run into issues with libraries so I haven't quite been able to start programming using one of the IDE's, as of now I'm still using Notepad++.  Also this week we started iintroducing print statements to the MiniSAT code to visualize how it is solving the SAT and began testing it on small, simple problems.  We were able to see where MiniSAT was making "assumptions" (instantiating a variable) and propagating other variables based on these assumptions, but we couldn't find a problem where we were able to see  MiniSAT backtracking.  We tried several Unsat problems with 100 or 200 variables and several constraints with no luck.  Fortunately, Dr. Dwyer found a SAT visualizer that came with a file that backtracked so we finally have been able to see how MiniSAT backtracks :).  We still want to make our own visualizer and will this upcoming week discuss what we like and don't like in the visualize Dr. Dwyer found (DPVIS – A Tool to Visualize the Structure of SAT Instances ). 

Further, Dr. Choueiry suggested that we look at how cconflicts are identified by CBJ,  test whether those conflicts are discovered more than once during search, and test whether they are global.  Perhaps this will be the topic of one of our posters :).

-Mary