Searcher::genRandomVarActMultDiv() too verbose

[a1880]

Routine Searcher::genRandomVarActMultDiv() (line 1608 in Searcher.cpp) emits quite a lot of messages. It tells about a difference which does not exist most of the time.

Example: c Using var act-multip 11 instead of standard 11 and act-divider 10 instead of standard 10

Well, it is just a tiny cosmetic issue, but ....

Greetings Axel

[msoos]

Good observation. It was an idea I had about varying the variable activity divider and multiplier. I think I will use that idea later and so I want to keep this inside. It's not too many lines that it generates and I kind of like it, as it reminds me that I need to work on that idea. I hope it's OK :)

Cheers,

mate

[a1880]

Ok. I have to confess that I am overwhelmed with the logging output of Cryptominisat. I find it not easy to understand and I would welcome any guidance or improvement. I always keep some level of verbosity active to get a feeling of what's going on. A real progress bar with "to complete in 26s" would be my eternal dream ;-)

Greetings

Axel

[msoos]

Hi,

You are right about the verbosity -- it's cluttered and hard to read. If you look at 'lingeling' it's somewhat better, though if you increase the verbosity, things also get out of hand there. Maybe if you have a look at the output of lingeling you could tell me what you think could be useful to impelement in CryptoMiniSat?

As for '26s remaining' -- that's of course impossible ;) Last time MiniSat had it, and people loved it. However, it course measured essentially nothing and was basically a random number. If we had an online database with terabytes of data and fast&accurate matching algorithm we could do something. However, I can create a problem that is megabytes in side and takes months to solve, but if I add 20 more literals the problem becomes 1 million times easier to solve. I think no matching algorithm will be able to handle that properly. I suggest we abandon this route for the moment and maybe concentrate on the verbosity.

Note that e.g. number of variables or number of binary clauses means nothing. I have seen problems that have millions of variables and solve in seconds and the smallest problem I saw that never terminated within any reasonable amount of time contained under 500 variables.

[a1880]

Hello, Please stop me, if this discussion gets too broad and philosophical. Basically, you are saying that logging information is rather meaningless for non-developer users like me and should be de-activated anyhow. Perhaps, it would be possible to restrict the information shown on the meaningful essentials: memory consumption, # of active threads, runtime. It would be sad and rather restricting/discouraging for common users if there were no measure for progress at all. At least, I'ld like to get a sort of life-sign to know that Cryptominisat is still up and running (= not died quietly or being caught in a non-productive endless loop).

Greetings

Axel

[msoos]

Hey,

I agree, it should have some of time/conflicts/propagations/number of free variables printed. It currently only prints conflicts and free varaibles, not propagations or time. lingeling prints time (maybe propagations too sometimes?), it would be interesting if you implemented that. Very easy, just hack void Searcher::print_restart_stat().

As for "progress" -- there is little we can do other than printing those 4. If you can accurately guess how much time it will take to solve, I think you have a good chance of winning some really big math prizes. I wish you luck with that, but I feel like there are other areas I would rather work on :)

As for non-productive loops: yeah, it would be nice. It's hard to know what is non-productive though, and even harder to detect it. However, it may be more possible than doing the progress bar.