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
No comments:
Post a Comment