December 2, 2009
by Connor Gallagher (cg09)

I’ll update all our excited readers on my personal progress over the last two weeks. I’ve been doing a lot of reading and code diving. My goal has been to see what other people are doing with restart strategies for SAT. In particular what information do they give their restart decision ie. information about solver state. I have discovered that the work done with restart strategies is very sparse when it comes to DPLL solvers. Apparently people do a lot more with search algorithms and restart procedures. So i did some research and some code diving and found that in most main stream SAT solvers the only information used in determining restarts is the number of backtracks. furthermore these strategies are mostly linear or rarely geometric. Another class of restart strategies are given by some sequence generated by a function.

I did not find any evidence of restart strategies using any more information than the number of backtracks. I would like to change this by allowing push to evolve restart strategies which can use other parameters. For example number of guessed variables, or some of the parameters used by the decision heuristic used in the solver ( i don’t understand these, but hey why not?), also information about the problem itself like clause number, or number of variables. Possibly big problems need more frequent restarts than little ones?

anyhow, I also looked at my verifier again, and cleaned it up a little. I also read over Marco’s code once it appeared a few hours ago. I’m not sure where we are with other things as I went out of town for the break and could not make contact with my partner when I returned. I assume this will all be reviled tomorrow in class.



November 10, 2009
by Connor Gallagher (cg09)

I would say this has been a good two weeks. I worked a little on a Parser for our SAT solver. Marco has been doing most of the coding and has finished our sat solver. I have been working on a lab report from hell also I have been reading over the documentation for our solver so that Marco’s thoughts may become intelligible to the rest of the world. We are using git for version management and our source code can be found here .

Decisions, Decisions…

October 21, 2009
by Marco Carmosino (malc07)

This week has been a good one for decisions. Essentially, we have found our evolutionary target, due to the fine paper linked here. In that paper, choice of static restart strategy is shown to seriously impact the profrmance of a modern, industrial-strength SAT solver, which they construct specifically to easily swap out the restart strategy code in. This was a 2007 paper, and there were only three followups that I could find 2008: one of them a formalization, one of them a human-produced dynamic restart strategy, and the last from the Constraint Satisfaction literature.

I propose that our project use push to evolve dynamic restart strategies. To focus on the restart strategy is a pooly-understood, recent innovation in SAT solver research. We are unsure exactly what the best restart strategies look like, even of their basic structure. This sounds like an excellent target for GP.

A decision remains to be made: I spent all week reading the code for minisat, picosat, and tinysat. I am of the opinion that it would be much more of a pain to instrument one of these existing sat sovlers than it would be to just write our own, based on tinysat, which is the solver used in the experiments from the original paper. They weigh in at only 600ish lines of code, and that’s in C++. Today, I will discuss this conclusion with conner and lee. I may be overlooking something, or it may indeed be a good idea.

By next week I hope to have a working SAT solver, one way or another.

Week 3

October 7, 2009
by Marco Carmosino (malc07)

This week, I have read and taken notes on four of Fukunaga’s papers. I have a much better grasp on his methods and research, mostly due to a 2008 summary paper. A 2004 paper by Fukunaga also provided an excellent abstract representation of the non-evolved heuristics for local search.  My main concern has been the distinction between:

  • evolving truth assignments for particular assignments (this is, essentially, stochastic local search in an evolutionary computation framework)
  • evolving heuristics for bit-flipping in stochastic local search algorithms (fukunaga’s work)
  • evolving heuristics for decision steps in DPLL
  • evolving programs which solve SAT

By far the most interesting point on the list above is that last one. To that end I have been looking for abstract state-space representations of the SAT problem from which to draw primitives. Conner found an excellent paper on DPLL that models the algorithm using a transition machine/rewrite system. This week, I will seek advice/references on using GP to evolve transition machines that could solve SAT.

Candidates for primitives include:

  • a “clause” stack, with operations:
    • A : (clause,truth-assignment) -> {t, if truth-assignment |= clause}
    • B : (clause,literal) -> {t, if literal is marked}
  • a “formula” stack
  • a “literal” stack
  • a “truth assignment” stack

I am unsure of the best way to represent transition machines in Push. Does it make sense to directly represent them in push code? Or should I make a “harness” push program that takes states and transitions from stacks and evolves them?

Week 3

October 7, 2009
by Connor Gallagher (cg09)

We have decided to peruse the SAT idea and drop all the others. Also we are both learning Earlang so we can hack things onto the cluster group’s push implementation. Personally my main pursuit over the last week has been learning Earlang.

Week 2

September 30, 2009
by Marco Carmosino (malc07)

This week, we took a good hard look at the SAT problem.

There are two ways to solve SAT efficiently: stochastic local search, and variants on the DPLL algorithm. I looked at local search, and Connor looked at DPLL. Today we’re going to compare notes.

I read the Fukunaga paper: it seems that using GP to evolve heuristics for which bit to flip next was a highly effective strategy. This is encouraging. I also got a textbook about stochastic local search in general, which has been useful for background.

It seems to me that a very useful contribution to the literature here could be an evolved DPLL/local search hybrid. My concern is that we could fall into the same trap that Fukunaga did in his first CLASS system, where sophisticated primitives didn’t buy him much at all. I will need to read that paper as well.

status report 1

September 22, 2009
by Connor Gallagher (cg09)

by connor

We met twice. We began considering some topics for research some of which are still a possibility  others do not appear to be suited for genetic programing. the topics we have been thing about are :

1. SAT solvers. We considered using GP to evolve a better SAT solver. This Idea has been abandoned because a SAT solver answers question which  does not have degrees of “correctness” but rather a binary true or false answer.

2. Linear Programing. still a possibility. This project would involve adding new functionality to Push.

3.  Automatic Theorem Proving. Again still a possibility, this problem is attractive because there is a wealth of data  on which we can test our program. We have also been searching our respective mathematical social networks for possible research topics. some literature:

Here is a link to our wiki. Feel free to create your own *Core on the ResearchCore page.