Mathematical Application of Push3

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.

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:

http://www.google.com/books?id=ynigSICJflYC&printsec=frontcover#v=onepage&q=&f=false

http://books.google.com/books?id=DN20_tW_BV0C&printsec=frontcover&client=firefox-a#v=onepage&q=&f=false

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