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

Week 2-3

These last few weeks we have continued our discussion about SAT problems.  After understanding the format of the benchmark problems and running into a few issues compiling MiniSAT, we finally got the benchmark problems to run on MiniSAT AND produce the correct results :).  We decided our next task is to dig into the MiniSAT code and try to understand how it works to solve the problems.  To do this we decided to form a graph displaying what steps the solver is taking to solve each benchmark.  We are in the process adding code to MiniSAT so that the graph is generated when the as the problem is being solved.  Eventually what we would like to do is have a sort of animation of how MiniSAT is solving a problem.  Right now, we are working to get the code compiling on our own computers (not using the CSE remote computer).

-Mary

Week One (Second Semester)

This week we started our weekly meetings again.  This semester we are planning on meeting twice weekly as a group.  Our meetings this semester will be more discussion based in comparison to last semester. This semester we are starting the SAT side of our research and including Elena and Dr. Dwyer in more in our discussions.  We have started comparing some of the techniques of both fields and are noticing that a lot of the same concepts exist in both fields.  For example a BCP (Boolean Constraint Propagation) in SAT is similar to the domino effect in CSPs.  For the first week we decided to explore SAT using a SAT solver, particularly miniSAT. As of right now, I have downloaded it and (finally) figured out how to compile it.  I plan on looking at some benchmark problems and trying to understand how it works J.

Kick-off meeting for Spring 2012

The entire team (2 ugrad students, Maggie and Mary, 2 grad mentors, Elena and Robert, and 2 faculty sponsors, Matt and Berthe) met for a relaxed meeting on January 6, 2012 at the Oven (Indian restaurant).  We discussed what was accomplished during Fall 2011 (where we focused on studying fundamental CP concepts and implementing search, backtracking, and consistency algorithms).  We agreed to start Spring 2012 by reverse engineering MiniSAT (SAT solver), studying SMT solvers, then diving into the study of constraints that arise in program analysis.  We will be meeting twice per week.  Most likely as follows: Once as a team to discuss progress and once as a smaller team to read tutorial papers.   Below is a photo of the super team taken at the Oven.  From left to right:  Elena, Matt, Berthe, Maggie, Robert,  and Mary.

End of semester meeting, Dec, 22, 2011

On December 22nd, 2011, we met at the Oven (Indian restaurant) for a relaxed brainstorming meeting.  Dr. Dwyer was in South Africa and could not join us.  Elena Sherman (graduate mentor) came to the restaurant, looked around for us, but could not find us although we were seated at the entrance (mishaps occur...), and left :-(   We are sorry, Elena, but we will coordinate better next time.  Were able to attend:  Mary, Maggie, Robert (graduate mentor), and Berthe.  During the dinner, we discussed the joys and difficulties of the fall semester and decided to delay any discussion about the Spring semester to another meeting that Matt and Elena can attend.  After the dinner, we took the photo below, which shows, from left to right, Robert, Mary, and Maggie.  Berthe took the photo.