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