[Cryptominisat-devel] Where to find removed variables ?

Martin Maurer meinemailingliste at online.de
Sam 15 Jan 11:51:46 CET 2011


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