Mathematical Application of Push3

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.

This entry was posted on October 21, 2009 at 11:48 am and is filed under Uncategorized.