Mathematical Application of Push3

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.

-Connor

This entry was posted on December 2, 2009 at 1:15 am and is filed under Uncategorized.