Incomplete Codebase

[zhaoyu-li]

Hi,

I find that in NLocalSAT/solvers/CPSparrow/CPSparrowp.sh, line 68, you want to use the neural network to initialize the assignment of a given SAT instance, however, you don't use the prediction file anymore. So actually, the solver doesn't use the neural network. And it seems like there is also a file called move_back.py in line 80 missing in this codebase.

Is there something wrong with your codebase or could you please provide the complete code?

[myxxxsquared]

Thanks for pointing out the problem in the code. I uploaded two required py files in the project, gen_predict.py, move_back.py. In the implementation, the solver does not call the neural network directly but uses prediction files, which contain the prediction of the neural network and the running time of the neural network. Prediction files could be generated using gen_predict.py.

[zhaoyu-li]

Thanks so much for your quick reply!

I know the solvers use prediction files, but as I mentioned before, in NLocalSAT/solvers/CPSparrow/CPSparrowp.sh, line 68, you want to use the neural network to initialize the assignment of a given SAT instance, however, you don't use the prediction file $predictFile anymore. And in your code of SLS solvers, you don't modify the solvers' code, so how can you implement Algorithm 3 in your paper, that is, initializing assignment with the predicted file when the solver needs restarts?

It seems like the folder of solvers is not up-to-date :)

Thanks in advance!

[myxxxsquared]

In solvers/Sparrow/sparrow.c:435, if USEPREDICT is defined, the solver will try to find the prediction file by appending '' in the end of the CNF file name, which is the same as $predictFile in solvers/CPSparrow/CPSparrowp.sh. I'll try to refine the code to make it easier to understand and use.

[zhaoyu-li]

Got it!

Thank you so much for your quick reply :)

[zhaoyu-li]

Hi Wenjie,

I notice that in NLocalSAT/solvers/CPSparrow/CPSparrowp.sh line 69, CPSparrow/bin/$satsolver -a -l -k -r1 $tmpCNF $seed > $model, you use the mode -k, which means keeping assignment after restart. However, if using that mode, Sparrow would not use the prediction of the neural network, since !keep_assig in NLocalSAT/solvers/Sparrow/sparrow.c line 602 is False.

Is there some misunderstanding or do we need to use the default mode?

[myxxxsquared]

I just checked the scripts used in experiments. During the evaluation of CPSparrow with prediction, I used CPSparrow_prepare.sh and then 'CPSparrow/code/Sparrow/sparrowp -a -l -r1 {problem} {seed}', instead of CPSparrowp.sh, because CPSparrowp.sh seems to output no correct solutions. Sorry for the unclear code. I will refine them recently.

[zhaoyu-li]

Got it! Thank you very much!