I want to get different solution every time I run minisat on the same problem. I can do that with using "rnd-seed" parameter of minisat. It simply randomize the variable selection so each time I can get different solution. Even though this parameter works perfectly on my machine (Ubuntu16) it does not work on gcloud (Google Cloud) running on Ubuntu machine.
I think I am missing a small part but I can not figure out what that is.
Note: I do not want to feed negotation of a solution to minisat to get different solution. I actually need to randomize the variable selection.
Edit: Let me explain why I need randomized solution. I solve lots of SAT problems and usually these SAT problems look like each other a lot. So, if I can not randomized variable selection, I get most of the time very similar solutions which I do not want. Therefore, I actually do not run minisat on the same problem.
Edit-2: @sascha wanted me to explain what I mean by "works" and "not works". When I run a cnf file on my PC, each time I get different solution. However, when I run the same cnf file on gcloud machine, I get always same solution.
The option -rnd-seed doesn't randomize branch variable selection. Rather, it allows you to set a seed for the pseudo-random number generator that Minisat uses.
Variable selection for branching does not involve randomness unless the -rnd-freq option is used. Pass in a floating point value between 0 and 1. 0 means no randomness, 1 means try to use a random variable every branch. The code only makes one attempt to choose a variable randomly, presumably because searching for an unset variable in an arbitrarily large priority queue can get pretty expensive. If that one attempt fails, Minisat branches using the normal priority queue.