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