Mathematical Application of Push3

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?

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