[Cryptominisat-devel] CNF permutations and running times

Martin Maurer meinemailingliste at online.de
Dim 2 Jan 08:27:00 CET 2011

Hello Vegard,

just some ideas:

- Have you checked that you always get the same solution ?
Otherwise i would say it is really luck that you one time get a solution 
the other time another solution slower. Can you perhaps go over all 
(depends on the number of solutions, i found at least 23 and then 
aborted...) ?
- When you have two runs, have you checks what times have a big difference ?
- Could the time to read cnf and output the solution have influence on total 
time ?
- Just for info: Which version have you used ? On which OS ? Which compiler 

Best regards and also happy new year,


----- Original Message ----- 
From: "Vegard Nossum" <vegard.nossum at gmail.com>
To: <cryptominisat-devel at lists.gforge.inria.fr>
Sent: Friday, December 31, 2010 7:18 PM
Subject: [Cryptominisat-devel] CNF permutations and running times


I was experimenting a bit with running times of the solver on
permutations of the same CNF formula. In this case, a permutation
means that literals within each clause are reordered and that the
clauses themselves are reordered. I would have expected that the
solver would use approximately the same amount of time for any
permutation of the formula, but clearly I was wrong. Here are my

Running the solver 100 times on the very same CNF file gave the
following results (CPU time):

 Min.   :10.03
 1st Qu.:10.15
 Median :10.33
 Mean   :10.39
 3rd Qu.:10.54
 Max.   :11.22

There is little variation so it looks pretty good. However, running
the solver 100 times, each time on a new random permutation of the
original CNF file, gave these results instead:

 Min.   : 3.160
 1st Qu.: 6.202
 Median : 9.875
 Mean   :10.218
 3rd Qu.:12.697
 Max.   :29.540

So the mean stayed about the same, but minimum and maximum times are
way out, an order of magnitudes apart. Is this behaviour expected? The
reason I ask is that I don't like the fact that literal and clause
order have so much to say for the running time, simply because it
_shouldn't_ matter for the difficulty of the problem. The problem is
in all essential ways the same.

One possible explanation is that in the case of the random
permutations, the solver simply made different choices, sometimes
lucky and sometimes unlucky. But why didn't this happen for the first
experiment (same file 100 times)? In that case, it means that the
solver's decisions depend on the order of literals and clauses. Is
that a good thing?

In any case, it seems that in order to get reliable timing experiments
with several runs on the same or similar formulas, they should be
randomly permuted before each solver run in order to get "better"
(closer to the truth) values for the running times.

The original CNF file, a "shuffle" program, raw data, and histograms
can be found at http://folk.uio.no/vegardno/shuffle.tar.bz2

Any other thoughts, ideas, explanations, etc. on the matter would be welcome 

Thanks, and happy new year :-)


Cryptominisat-devel mailing list
Cryptominisat-devel at lists.gforge.inria.fr

More information about the Cryptominisat-devel mailing list