2

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.

one
  • 62
  • 5
  • This approach has probably no guarantees at all. Are you really sure that's the way too go? – sascha Jun 08 '18 at 20:03
  • I am open to other suggestions as well. All I need to do is to get a different solution. But the different solution must be totally randomized. I always used this approach on my machine and other several servers. It always worked. – one Jun 08 '18 at 20:07
  • If totally randomized means: uniformly sampled, you are on the wrong path (it's not going to work like that!). You will find some (potentially scary) information [here](https://stackoverflow.com/a/47208133/2320035). – sascha Jun 08 '18 at 20:09
  • Yeah I can understand that. Totally randomized is scary :) I used the wrong word. Let me correct myself. I only need to randomize variable selection with basic randomization techniques, not cryptographically randomize. – one Jun 08 '18 at 20:14
  • You do not seem to understand what i'm saying. How much do you know about SAT-solvers, algorithmics, NP-hardness and co.? How scientific is your work? What you do, well, it will fail on many many problems. But until now, there is not even a real specification: uniform-sampling, which is one thing people sometimes try to achieve has nothing to do with PRNG vs. cryptoPRNG. (CDCL) SAT-solvers are heuristics and are highly biased. Variable-selection is not changing all that (but sometimes it looks like that; of course heavily dep on problem). Read the paper mentioned in my link and be precise! – sascha Jun 08 '18 at 20:17
  • And ignoring all those theoretical issues: explain what *works* and *works not* means exactly. Then describe the setup and compilation-process (involving the tools and versions) and maybe even how you use the solver. Depending on the usage, my first step would be replacing Minisat with something more maintained like cryptominisat. – sascha Jun 08 '18 at 20:30
  • I think we are getting off the topic. I am not expert at SAT solvers. Minisat states that "-rnd-seed: Used by the random variable selection". I want to use this feature of minisat. I don't understand why we are talking about these kinds of things. I am saying that it works for my PC but does not work on gcloud. – one Jun 08 '18 at 22:01
  • And as i said: i'm just warning you about the theory-side (to not waste time) and told you, that for debugging this, no specific details on OS, Architecture and Setup is given. – sascha Jun 08 '18 at 22:02
  • Exactly, that's what I am guessing as well. It should not be dependent on these things (OS etc). Therefore, I said in the question that I am missing a small part but I don't know what that is. – one Jun 08 '18 at 22:07
  • Anyway, I think I need to figure out the problem on my own. I will play a little more. If I can find the problem, let you know. – one Jun 08 '18 at 22:08

1 Answers1

1

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.

Kyle Jones
  • 5,492
  • 1
  • 21
  • 30
  • For some reason, I have lost access to my gcloud account. As soon as I connect again, I will try and let you know result. – one Jun 09 '18 at 21:08