search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
816 stars 180 forks source link

Impact of Clauses Order on The Performance #620

Closed hadipourh closed 4 years ago

hadipourh commented 4 years ago

Dear Mate,

Hope you are fine. I am curious to know, whether the order of printed clauses within a given CNF file, has any considerable impact on the performance? In other words, does the order of writing clauses in a CNF file, have any effect on solving time, when CryptoMinisat is used as the solver? I am asking this, since I have observed a similar effect in other constraint programming solvers, and I am wondering that whether CryptoMinisat has such an issue as well or not? The answer of this question is too important for me, because, for my new cryptanalysis tool, I am seeking out for a new solver, which it's performance must be independent of constraints order. Thank you for creating the CryptoMinisat, and thank you in advance for your help.

Kind regards, Hosein

msoos commented 4 years ago

Hi,

No SAT solver has independent performance of the order of clauses. Absolutely, and totally, none. I have been doing this for 10+ years, believe me. So, now that's out of the way. The best way to do good, solid understanding of the approximate average time to solve is to do the following:

Done. Your timings will be incredibly solid. If you don't randomize you will get something like:

10b needs to be broken: 10s 11b needs to be broken: 4s 12b needs to be broken: 1634s 13b needs to be broken: 138s 14b needs to be broken: 198738s 15b needs to be broken: 2994s

in other words, complete, utter, garbage. Total trash. You will see this kind of "science" in published research papers and you will realize what utter nonsense they are doing. If you instead do the randomized average (do NOT randomize clause order, instead, randomize input!) you will get:

10b: 10.1s 11b: 15.15s 12b: 22.74s 13b: 34.08s 14b: 51.13s

etc. in other words, it will make absolute, total, complete sense

Good luck randomizing your input. If you do anything else, you'll get the timings I had in the previous table. If you want to do science, do the 2nd table.

Good luck using CryptoMiniSat,

Mate

hadipourh commented 4 years ago

Hello Mate!

Thanks for your complete, and helpful answer. If I understand well, according to your first sentence, the performance of all SAT solvers depends on the order of clauses (constraints) inside the given CNF file.

Regarding your examples and measuring the solving time, I agree. We must report the average of consumed times in several experiments where input/output data are chosen uniformly random in each one. I believe you, as the one who is very experienced in this field, and I appreciate your time for sharing your great experiences with others.

Although reporting the correct timing is important, the current problem is the performance not measuring the time only. I am facing with a problem in which the order of clauses has a great impact on the solving time. According to my observations, there might be a huge difference between the solving time of two same CNFs, which are only different from the "order of clauses" point of view, and nothing else.

This fact (effects of clauses order on the performance), arises the following important questions:

1- How much impact does the order of clauses have on the performance? 2- How to choose an almost appropriate order to improve the performance?

Thank you for your time, and sharing your valuable experiences.

Kind regards, Hosein

msoos commented 4 years ago

You can't improve performance. Just let go of this idea. You can't. Those questions are meaningless to answer. It's like asking how to throw the uniformly random dice to get a 6? I believe trying to answer that question may lead one to become a junkie at a Las Vegas Casino.

Sorry, but I can't help you anymore. Good luck trying to optimize a random rice,

Mate

On Fri, Jun 26, 2020, 09:24 Hosein Hadipour notifications@github.com wrote:

Hello Mate!

Thanks for your complete, and helpful answer. If I understand well, according to your first sentence, the performance of all SAT solvers depends on the order of clauses (constraints) inside the given CNF file.

Regarding your examples and measuring the solving time, I agree. We must report the average of consumed times in several experiments where input/output data are chosen uniformly random in each one. I believe you, as the one who is very experienced in this field, and I appreciate your time for sharing your great experiences with others.

Although reporting the correct timing is important, the current problem is the performance not measuring the time only. I am facing with a problem in which the order of clauses has a great impact on the solving time. According to my observations, there might be a huge difference between the solving time of two same CNFs, which are only different from the "order of clauses" point of view, and nothing else.

This fact (effects of clauses order on the performance), arises the following important questions:

1- How much impact does the order of clauses have on the performance? 2- How to choose an almost appropriate order to improve the performance?

Thank you for your time, and sharing your valuable experiences.

Kind regards, Hosein

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/620#issuecomment-650023733, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAKF4ONUIXUFSQTZVHW3QCTRYREMNANCNFSM4OIQJA5Q .

hadipourh commented 4 years ago

Dear Mate,

Saying that my questions are meaningless is an excellent answer by itself! So I will not try to find the answer according to your kind advice and I will save time. I didn't know they are meaningless to be honest.

You must know that I am a newbie in this field, and I have not a bad intention if I ask a question. The only purpose I have, is knowing more, nothing else. I didn't know the order of clauses must have an impact on the performance. This fact might be trivial from your point of view as an experienced person, but this is a new observation for me as the one who is newbie in this field.

All in all, thanks for your time, and answering my questions.

Kind regards, Hosein

a1880 commented 4 years ago

It might be of interest to have a look at this related paper.