feiwang3311 / MCTSminisat

minisat within MCTS
Other
3 stars 2 forks source link

The neural network implementation seems to be incomplete #1

Closed xuruiyang closed 5 years ago

xuruiyang commented 5 years ago

Hello Feiwang,

I tried to use your minisatMCTS on some SAT problems, but it turns out that the program didn't work. I notice that there is no interaction between the neural network and your implementation. I thought the program might be incomplete. Would you mind to upload the complete version of your program?

Thanks!

feiwang3311 commented 5 years ago

Hi,

The minisatMCTS repo is only intended to provide MCTS-style simulation, and a Python interface to use the solver as a RL playground. I should have a description about it but I haven't been woking on this repo for quite a while, and this repo is not popular anyway.

The NN that uses the minisatMCTS code is here: https://github.com/feiwang3311/baseline/tree/sat/baselines/MCTS

Again there is not much description of what is going on. The code is not ready to run without modification.

Do you mind telling me what do you need from these repo? i might be of more help in that case.

xuruiyang commented 5 years ago

Thank you so much for your help!

I was recently doing researches in solving combinatorial problems with deep learning. I came up to your workshop paper online (https://arxiv.org/abs/1802.05340) and found that could be an interesting research spot.

For the time being, I just like to try your implementation and reproduce the results you have shown in your paper.

feiwang3311 commented 5 years ago

I see. I personally do not think high of that archive paper. It was rejected by ICLR last year. There are many problems to it.

First of all, the simulation-based decision is very expensive. It is almost impossible to benefit from the decision due to the overhead. Second, the training result looks very good, but it may be due to very small SAT problems used (20 vars, 96 clauses). In that case simulation helps a lot. But I seriously doubt that the training result is still that good for larger SAT formula. Third, the paper used CNN to embed the SAT formula, which is wrong in many ways. A better way is to use GNN.

The other link I sent to you has the NN code that uses the minisatMCTS. You can take a look. You may need to copy the file in the save_sim dir out to run it. It is basically a bunch of Python files that run AlphaGo style RL in a synchronous manner. Let me know if any part of the code is not clear. To reproduce the result in the paper is not hard, but I just didn't attend my repo well, and there might be errors when running. If you like to chat over any errors, maybe it is easier to ping me at wang603@purdue.edu or get me by hangout (feiwang3311@gmail.com) or wechat (wang603purdue).

As I said, I do not think high of that archive paper. Nor do I think ML for combinatorial problems is a profitable direction. We can chat more over it if you like. I might be a little narrow-minded on this matter. :)

xuruiyang commented 5 years ago

Thanks for your help, I'm greatly appreciated! I will let you know if I have further problems with running the program.

dmeoli commented 6 months ago

Hi,

The other link I sent to you has the NN code that uses the minisatMCTS.

@feiwang3311 how can I reproduce the results of the paper? Can u share the same materials also with me?

Thanks for your help, I'm greatly appreciated! I will let you know if I have further problems with running the program.

@xuruiyang were you able to develop a working version of the code?

thx