Incomplete Codebase about nlocalsat HOT 7 CLOSED

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.

from nlocalsat.

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!

from nlocalsat.

In solvers/Sparrow/sparrow.c:435, if USE_PREDICT 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.

from nlocalsat.

Got it!

Thank you so much for your quick reply :)

from nlocalsat.

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?

from nlocalsat.

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.

from nlocalsat.

Got it! Thank you very much!

from nlocalsat.