[Cryptominisat-devel] Where to find removed variables ?

Martin Maurer meinemailingliste at online.de
Sam 15 Jan 12:11:26 CET 2011


Sorry, was old version of cryptominisat. But newest show same behaviour...
(but i think it is not cryptominisat-related, because in 10x10 there are 100 
variables removed, in 8x8 i see a 64 variables removal.
I tend to say i have a bug in cnf generation...)

Nevertheless here is the output of the todays version (cluser 129 fixed):

cryptominisat64 --dumplearnts=10x10_learnt_1.cnf --maxdumplearnts=2 --dumporig=10x10_dumporig_1.cnf 
10x10_new_jan2011.cnf
c Outputting solution to console
c This is CryptoMiniSat Jan 11 2011
c Reading file '10x10_new_jan2011.cnf'
c -- clauses added:            0 learnts,     10682740 normals,            0 
xors
c -- vars added      17056
c Parsing time:  3.65 s
c  N st     0         0     17056       100  10682640         0  21382336 
0   no data   no d
ata
c asymm  cl-useful: 0/100/100 lits-rem:0 time: 0.01
c Flit:     0 Blit:      0 bXBeca:    0 bXProp:    0 Bins:      0 BRemL: 
0 BRemN:      0 P: 54.
4M T:  3.80
c blocked clauses removed:        0 vars:      0 tried:       17056 T: 0.02 
s
c bin-w-bin subsume rem            0 bins  time:  3.49 s
c subs with bin:        0  lits-rem:         0  v-fix:    0  time:  4.80 s
c Subs w/ non-existent bins:      0 l-rem:      0 v-fix:     0 done:  17056 
time:  0.86 s
c Removed useless bin:       0  fixed:     0  props:  20.00M  time:  0.44 s
c lits-rem:       635  cl-subs:        0  v-elim:    100  v-fix:    0  time: 
3.30 s
c Finding binary XORs  T:     0.50 s  found:       0
c Finding non-binary XORs:     0.47 s (found:       0, avg size: -1.$)
c calculated reachability. Time: 0.29
c Calc default polars -  time:   0.10 s pos:       0 undec:     100 neg: 
16956
c 
=========================================================================================
c types(t): F = full restart, N = normal restart
c types(t): S = simplification begin/end, E = solution found
c restart types(rt): st = static, dy = dynamic
c  t rt  Rest     Confl      Vars   NormCls    BinCls   Learnts    ClLits 
LtLits
c  B st     0         0     16956     74140  10591544         0  38264113 
0   no data   no d
ata
c  N dy    19      4108     16956     74140  10591836      3810  38264113 
212266      7.72      8
.57
c  N dy    44      8285     16956     74140  10591997      5597  38263880 
258971      8.95      9
.59
c  N dy    69     12391     16956     74140  10592159      5965  38263851 
185969      9.45     10
.16
c  N dy    99     16429     16956     74140  10592330      9826  38263850 
523095     10.07     11
.71
c  N dy   132     20453     16956     74140  10592478      9528  38263837 
331932     10.42     11
.25

*** INTERRUPTED ***
*** Please wait. We need to interrupt cleanly
*** This means we might need to finish some calculations
c Sorted learnt clauses dumped to file '10x10_learnt_1.cnf'
c Simplified original clauses dumped to file '10x10_dumporig_1.cnf'
c Not finished running -- maximum restart reached
c num threads              : 1
c restarts                 : 138
c dynamic restarts         : 132
c static restarts          : 6
c full restarts            : 0
c total simplify time      : 0.01
c learnts DL2              : 0
c learnts size 2           : 10683610
c learnts size 1           : 0           (0.00      % of vars)
c filedLit time            : 3.81        (5.98      % time)
c v-elim SatELite          : 100         (0.59      % vars)
c SatELite time            : 7.58        (11.89     % time)
c v-elim xor               : 0           (0.00      % vars)
c xor elim time            : 0.00        (0.00      % time)
c num binary xor trees     : 0
c binxor trees' crown      : 0           (-1.#J     leafs/tree)
c bin xor find time        : 0.50
c OTF clause improved      : 29          (0.00      clauses/conflict)
c OTF impr. size diff      : 309         (10.66      lits/clause)
c OTF cl watch-shrink      : 20878       (0.97      clauses/conflict)
c OTF cl watch-sh-lit      : 3124932     (149.68     lits/clause)
c tried to recurMin cls    : 5165        (24.01      % of conflicts)
c updated cache            : 0           (0.00       lits/tried recurMin)
c clauses over max glue    : 0           (0.00      % of all clauses)
c conflicts                : 21511       (337.54    / sec)
c decisions                : 649987      (0.00      % random)
c bogo-props               : 864166375   (13560017.81 / sec)
c conflict literals        : 1591506     (71.35     % deleted)
c Memory used              : 0.00        MB
c CPU time                 : 63.73       s


----- Original Message ----- 
From: "Martin Maurer" <meinemailingliste at online.de>
To: <cryptominisat-devel at lists.gforge.inria.fr>
Sent: Saturday, January 15, 2011 11:51 AM
Subject: Where to find removed variables ?


> Hello Mate,
>
> i download cluster129 fixed and compiled, so far everything is working, no 
> complaints, no crashes so far during calculation (but not used it very 
> often yet).
>
> However i have a situation, which i think i have never seen before. 
> Perhaps you can clarify.
> Perhaps i have also done an error in generating cnf, so it could be it has 
> nothing to do cryptominisat at all.
>
> I have generated a cnf for a 10x10 puzzle, named 10x10_new_jan2011.cnf:
> It has 17056 variables and as usual for my puzzles a lot of clauses.
>
> I call it the following, but abort it after some short time:
>
> cryptominisat64 --dumplearnts=10x10_learnt_1.cnf --maxdumplearnts=2 --dumporig=10x10_dumporig_1.cnf 
> 10x10_new_jan2011.cnf
> c Outputting solution to console
> c Using 4 threads
> c This is CryptoMiniSat Nov 18 2010
> c Reading file '10x10_new_jan2011.cnf'
> c -- clauses added:            0 learnts,     10682740 normals, 
> 0 xors
> c -- vars added      17056
> c Parsing time:  3.79 s
> c  N st     0         0     17056       100  10682640         0  21382336 
> 0   no data   no d
> ata
> c asymm  cl-useful: 0/100/100 lits-rem:0 time: 0.01
> c Flit:     0 Blit:      0 bXBeca:    0 bXProp:    0 Bins:      0 BRemL: 0 
> BRemN:      0 P: 54.
> 4M T:  3.72
> c bin-w-bin subsume rem            0 bins  time:  3.64 s
> c subs with bin:        0  lits-rem:         0  v-fix:    0  time:  4.80 s
> c Subs w/ non-existent bins:      0 l-rem:      0 v-fix:     0 done: 
> 17056 time:  0.85 s
> c Removed useless bin:       0  fixed:     0  props:  20.00M  time:  0.45 
> s
> c lits-rem:         0  cl-subs:        0  v-elim:    100  v-fix:    0 
> time: 3.74 s
> c Finding binary XORs  T:     0.08 s  found:       0
> c Finding non-binary XORs:     0.49 s (found:       0, avg size: -1.$)
> c Calc default polars -  time:   0.11 s pos:       0 undec:     100 neg: 
> 16956
> c 
> =========================================================================================
> c types(t): F = full restart, N = normal restart
> c types(t): S = simplification begin/end, E = solution found
> c restart types(rt): st = static, dy = dynamic
> c  t rt  Rest     Confl      Vars   NormCls    BinCls   Learnts    ClLits 
> LtLits
> c  B st     0         0     16956     74140  10591544         0  38264748 
> 0   no data   no d
> ata
> c  N dy    12      4094     16956     74140  10592501      3582  38264737 
> 182792     12.23     15
> .36
> c  N dy    19      8188     16956     74140  10592885      4931  38264563 
> 180679     10.36     13
> .36
>
> *** INTERRUPTED ***
> *** Please wait. We need to interrupt cleanly
> *** This means we might need to finish some calculations
> c Sorted learnt clauses dumped to file '10x10_learnt_1.cnf'
> c Simplified original clauses dumped to file '10x10_dumporig_1.cnf'
> c restarts              : 27
> c dynamic restarts      : 21
> c static restarts       : 6
> c full restarts         : 0
> c learnts DL2           : 0
> c learnts size 2        : 10684048
> c learnts size 1        : 0           (0.00      % of vars)
> c filedLit time         : 3.73        (7.49      % time)
> c v-elim SatELite       : 100         (0.59      % vars)
> c SatELite time         : 8.16        (16.40     % time)
> c v-elim xor            : 0           (0.00      % vars)
> c xor elim time         : 0.00        (0.00      % time)
> c num binary xor trees  : 0
> c binxor trees' crown   : 0           (-1.#J     leafs/tree)
> c OTF clause improved   : 10          (0.00      clauses/conflict)
> c OTF impr. size diff   : 220         (22.00      lits/clause)
> c OTF cl watch-shrink   : 9517        (0.97      clauses/conflict)
> c OTF cl watch-sh-lit   : 1574675     (165.46     lits/clause)
> c tried to recurMin cls : 1053        (10.78      % of conflicts)
> c updated cache         : 0           (0.00       lits/tried recurMin)
> c num threads           : 4
> c num units recevied    : 0           (-1.#J     % of units)
> c num units sent        : 0           (-1.#J     % of units)
> c num bins recevied     : 1008
> c num bins sent         : 2009782813
> c clauses over max glue : 737         (7.54      % of all clauses)
> c conflicts             : 9771        (196.33    / sec)
> c decisions             : 410672      (0.00      % random)
> c bogo-props            : 437213410   (8784854.23 / sec)
> c conflict literals     : 693953      (73.16     % deleted)
> c Memory used           : 0.00        MB
> c CPU time              : 49.77       s
>
>
> As you can see the number of variables was reduced from 17056 to 16956 
> (100 variables less).
>
> Perhaps two hints, where i see the number "100":
>
> c Removed useless bin:       0  fixed:     0  props:  20.00M  time:  0.45 
> s
> c lits-rem:         0  cl-subs:        0  v-elim:    100  v-fix:    0 
> time: 3.74 s
>
> and
>
> c v-elim SatELite       : 100         (0.59      % vars)
>
> I am happy to find 100 variables (their value), but where can i find which 
> variables were set to which value ?
>
> Looking into learnt clause file, i see the following (complete file, but 
> taking binary clauses out, too long):
>
> c
> c ---------
> c unitaries
> c ---------
> c conflicts 9771
> c
> c ---------------------------------
> c learnt binary clauses (extracted from watchlists)
> c ---------------------------------
> -1 -357 0
> -1 -277 0
> 2 -250 0
> 2 -246 0
> 2 -248 0
> ...
> -17034 17055 0
> -17036 17055 0
> -17038 17055 0
> c
> c ---------------------------------------
> c clauses representing 2-long XOR clauses
> c ---------------------------------------
> c
> c --------------------
> c clauses from learnts
> c --------------------
>
> So there i see no "unitaries" (is this the right word, for what i am 
> looking for ?).
>
> Are these 100 unitaries missing in learnt clause file ? Or must i look 
> somewhere else ?
> Or is there another reason why they were removed, e.g. does it look like 
> this, when variable was not used in clauses at all ?
>
> Best regards,
>
> Martin
>
> 




More information about the Cryptominisat-devel mailing list