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 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?

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.