search

msoos / cryptominisat

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

xor-together takes a long time #601

Closed sfiruch closed 4 years ago

sfiruch commented 4 years ago

For the input min5.zip the latest CMS takes surprisingly long in the xor-together stage. It sits there for many minutes. Perhaps this is expected, perhaps it's an O(n^2) algorithm rearing its head.

I ran the current CMS version with GAUSS from https://ci.appveyor.com/project/msoos/cryptominisat/build/job/5snfkq3y53od6grt/artifacts. Here's the log where the solver is stuck in xor-together:

c CryptoMiniSat version 5.6.8
c CMS Copyright Mate Soos (soos.mate@gmail.com)
c CMS SHA revision e440d535cb4500706b38ec5d655111a735dbb60e
c CMS is MIT licensed
c Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'
c       by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos
c CMS compilation env CMAKE_CXX_COMPILER = C:/Program Files (x86)/Microsoft Visual Studio/2017/Community/VC/Tools/MSVC/14.16.27023/bin/Hostx86/x64/cl.exe | CMAKE_CXX_FLAGS = /DWIN32 /D_WINDOWS /W3 /GR /EHsc | COMPILE_DEFINES =  -DUSE_GAUSS -DNDEBUG -D_FORTIFY_SOURCE=0 | STATICCOMPILE = ON | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND =  | ZLIB_FOUND =  | VALGRIND_FOUND =  | ENABLE_TESTING = OFF | M4RI_FOUND = FALSE | NOM4RI = OFF | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = OFF | PYTHON_EXECUTABLE = C:/Python36-x64/python.exe | PYTHON_LIBRARY = C:/Python36-x64/libs | PYTHON_INCLUDE_DIRS = C:/Python36-x64/include | MY_TARGETS =  | LARGEMEM = OFF | LIMITMEM = OFF | compilation date time = Dec 23 2019 21:23:50
c CMS compiled with non-gcc compiler
c Executed with command line: cryptominisat5.exe min5.dimacs
c Reading file 'min5.dimacs'
c -- header says num vars:         462820
c -- header says num clauses:     1289852
c -- clauses added: 1289852
c -- xor clauses added: 0
c -- vars added 462820
c Parsing time: 0.48 s
c   type VSIDS  rest  conf freevar  IrrL  IrrB l/longC  l/allC RedL0 RedL1 RedL2  RedB l/longC  l/allC
c [distill] long cls tried: 28/28 cl-short:28 lit-r:0 T: 0.00 T-out: N T-r: 100.00%
c [distill] long cls tried: 1476/1415 cl-short:1476 lit-r:169 T: 0.00 T-out: N T-r: 99.95%
c [distill] long cls tried: 1733/3060 cl-short:1733 lit-r:170 T: 0.00 T-out: N T-r: 99.94%
c   glue     1    39  8193  462791  671K  618K    3.52    2.79  3832  2489   791  1070    5.11    4.71
c [distill] long cls tried: 3189/6065 cl-short:3189 lit-r:635 T: 0.01 T-out: N T-r: 99.88%
c   geom     1    83 16386  462777  671K  618K    3.52    2.79  8117  4438  1531  2275    5.46    4.98
c [distill] long cls tried: 2208/8097 cl-short:2208 lit-r:353 T: 0.01 T-out: N T-r: 99.91%
c [distill] long cls tried: 4221/12011 cl-short:4221 lit-r:1080 T: 0.02 T-out: N T-r: 99.81%
c   glue     1   107   24K  462738  671K  618K    3.52    2.79 12569  5728  2616  3622    5.66    5.12
c [distill] long cls tried: 4742/15584 cl-short:4197 lit-r:1918 T: 0.13 T-out: N T-r: 98.54%
c   glue     1   137   32K  460844  671K  618K    3.52    2.79 16172  7638  2729  4856    5.68    5.11
c   glue     1   146   40K  456173  671K  618K    3.52    2.79   22K  6528  4804  5541    5.95    5.40
c [distill] long cls tried: 6896/20723 cl-short:5941 lit-r:2651 T: 2.56 T-out: N T-r: 87.83%
c   glue     1   158   49K  454017  671K  618K    3.52    2.79   25K  9541  3483  6837    5.72    5.15
c [distill] long cls tried: 7894/27298 cl-short:7414 lit-r:3584 T: 5.65 T-out: N T-r: 77.84%
c   geom     1   181   57K  451768  671K  618K    3.52    2.79   29K  8394  6178  8229    6.23    5.57
c   glue     1   195   65K  450133  671K  618K    3.52    2.79   35K  7822  6255  8677    6.19    5.57
c [distill] long cls tried: 8945/35090 cl-short:8639 lit-r:4656 T: 11.17 T-out: N T-r: 65.00%
c recursive minimization cost OK: 342Kcost/(% lits removed)
c more minimization effectiveness low: 0.00 % lits removed --> disabling
c --> Executing strategy token: handle-comps
c --> Executing strategy token: scc-vrepl
c [scc] new: 1 BP 1M T: 0.06
c --> Executing strategy token: cache-clean
c --> Executing strategy token: cache-tryboth
c --> Executing strategy token: sub-impl
c [impl sub] bin: 2863 T: 0.06 T-out: N w-visit: 925640
c --> Executing strategy token: intree-probe
c [scc] new: 10 BP 1M T: 0.05
c [vrep] vars 10 lits 178 rem-bin-cls 46 rem-long-cls 3 BP 2M T: 0.05
c [scc] new: 2 BP 1M T: 0.05
c [vrep] vars 2 lits 35 rem-bin-cls 10 rem-long-cls 0 BP 2M T: 0.04
c [scc] new: 0 BP 1M T: 0.05
c [vrep] vars 0 lits 0 rem-bin-cls 0 rem-long-cls 0 BP 2M T: 0.04
c [intree] Set 6 vars hyper-added: 131906 trans-irred::97 trans-red::177 T: 11.26 T-out: Y T-r: -4.75%
c --> Executing strategy token: probe
c --> Executing strategy token: sub-str-cls-with-bin
c [distill] cache-based irred--  cl tried  1280129 cl-sh 24855 cl-rem 12319 lit-rem  25094 T: 1.06 T-out: N
c [distill] cache-based   red--  cl tried    70414 cl-sh   648 cl-rem 1279 lit-rem    852 T: 0.06 T-out: N
c --> Executing strategy token: distill-cls
c [distill] long cls tried: 14552/632251 cl-short:2774 lit-r:1411 T: 2.84 T-out: Y T-r: -0.01%
c [distill] long useful: 5548/29104/1265792 lits-rem: 2822 0-depth-assigns: 36 T: 5.69 T-out: Y
c --> Executing strategy token: scc-vrepl
c [scc] new: 33 BP 1M T: 0.06
c --> Executing strategy token: sub-impl
c [impl sub] bin: 91 T: 0.06 T-out: N w-visit: 925640
c --> Executing strategy token: str-impl
c [impl str] lit bin: 0 (by stamp: 0) set-var: 0 T: 0.04 T-out: N T-r: 95.49% w-visit: 925640
c --> Executing strategy token: sub-impl
c [impl sub] bin: 0 T: 0.06 T-out: N w-visit: 925640
c --> Executing OCC strategy token(s): 'occ-backw-sub-str,occ-clean-implicit,occ-bve,occ-bva,occ-ternary-res,occ-xor,'
c [occ] mem usage for occur     67 MB
c [occ] mem usage for occur     36 MB
c Mem for watch alloc      : 38          MB (0.00      %)
c Mem for watch array      : 21          MB (0.00      %)
c --> Executing OCC strategy token: occ-backw-sub-str
c [occ-backw-sub-str-long-w-bins] subs: 384 str: 2094 tried: 1472593 0-depth ass: 0 T: 0.19 T-out: N T-r: 81.56%
c [occ-sub-long-w-long] rem cl: 26724 tried: 1357368/678684 (200.0%) T: 0.58 T-out: N T-r: 64.97%
c [occ-sub-str-long-w-long] sub: 150 str: 2774 tried: 2036052/678684 (300.0)  T: 1.08 T-out: N T-r: 25.98%
c [occ-sub-str-w-added-long]  sub: 0 str: 0 0-depth ass: 0 T: 0.00 T-out: N T-r: 99.65%
c --> Executing OCC strategy token: occ-clean-implicit
c --> Executing OCC strategy token: occ-bve
c [occ-empty-res] Empty resolvent elimed: 131411 T: 0.09 T-out: N
c [occ-bve] iter v-elim 172141
c cl_inc_rate=0.7, var_dec_rate=2.2 (grow=0)
c Reduced to 145114 vars, 893018 cls (grow=0)
c x n vars       : 145114
c  #try to eliminate:   437K
c  #var-elim        :   172K
c  #T-o: N
c  #T-r: 99.44%
c  #T  : 2.84
c [occur] 0.42 is overhead
c [occur] link-in T: 0.42 cleanup T: 0.00
c --> Executing OCC strategy token: occ-bva
c [occ-bva] global numcalls: 0
c --> Executing OCC strategy token: occ-ternary-res
c --> Executing OCC strategy token: occ-xor
c [occ-xor] sort occur list T: 0.06
c [occ-xor] found  49204 avg sz 3.4 min sz  3 max sz  4 T: 0.41 T-out: N T-r: 99.35%
c [xor-together] xored together 48926 xors orig num xors: 49204 T: 677.63
c [xor-add-lem] added unit 0 bin 0 T: 0.00
c --> Executing strategy token: cl-consolidate
c [mem] consolidate  old-sz:    46M new-sz:    22M new bits offs: 0 T: 0.09
c --> Executing strategy token: str-impl
c [impl str] lit bin: 5 (by stamp: 0) set-var: 6 T: 0.05 T-out: N T-r: 97.70% w-visit: 925640
c --> Executing strategy token: cache-clean
c --> Executing strategy token: sub-str-cls-with-bin
c [distill] cache-based irred--  cl tried   591220 cl-sh     0 cl-rem 1582 lit-rem      0 T: 0.55 T-out: N
c [distill] cache-based   red--  cl tried    33680 cl-sh     8 cl-rem    4 lit-rem      8 T: 0.03 T-out: N
c --> Executing strategy token: distill-cls
c [distill] long cls tried: 20657/576431 cl-short:4096 lit-r:709 T: 3.17 T-out: Y T-r: -0.04%
c [distill] long useful: 8192/41314/1153384 lits-rem: 1418 0-depth-assigns: 0 T: 6.34 T-out: Y
c --> Executing strategy token: scc-vrepl
c [scc] new: 27 BP 0M T: 0.06
c --> Executing strategy token: check-cache-size
c --> Executing strategy token: renumber
c [xor-clean] T: 0.00
c [renumber] T: 0.36
c --> Executing strategy token: sls
c [consolidate] mini T: 0.00
c global_timeout_multiplier: 4.40
c clause size stats. size3: 344904 size4: 210543 size5: 19563 larger: 1421
c [xor-rem-unconnected] left with 49201 xors from 49204 non-empty xors T: 0.01
c [xor-together] xored together 48926 xors orig num xors: 49201 T: 790.00
c [xor-rem-unconnected] left with 214 xors from 275 non-empty xors T: 0.00
c [matrix] Good   matrix  0    209 x14133  density:  0.0%  xorlen avg: 69.61  perc sampl: 0.000 %
c [matrix] Good   matrix  1      5 x 7991  density:  0.2%  xorlen avg: 1599.80  perc sampl: 0.000 %
c Found matrixes: 2 from 214 xors T: 790.03 T-out: N
c [xor-add-lem] added unit 0 bin 0 T: 0.00
c [xor-add-lem] added unit 0 bin 0 T: 0.00
c   luby     0   223   73K  145027  576K  314K    3.44    2.93 19046  6970   578   45K    4.88    3.07
c [matrix] Disabling ALL GJ-elim in this round.  Usefulness was: 0.00%
c   luby     0   255   81K  144768  576K  314K    3.44    2.93   25K  4572  4609   45K    5.31    3.42
c [distill] long cls tried: 10646/24970 cl-short:10370 lit-r:2551 T: 4.21 T-out: N T-r: 85.81%
c   luby     0   273   90K  144134  576K  314K    3.44    2.93   30K  4922  4421   46K    5.15    3.46
c   luby     0   305   98K  143942  576K  314K    3.44    2.93   34K  7647  5921   46K    6.63    4.35
c [distill] long cls tried: 13426/37353 cl-short:13151 lit-r:6155 T: 8.12 T-out: N T-r: 75.06%
c   luby     0   330  106K  143898  576K  314K    3.44    2.93   39K  8308  5450   47K    7.66    4.99
c   luby     0   331  114K  143878  576K  314K    3.44    2.93   45K  7550  8303   47K    7.97    5.35
c   luby     0   362  122K  143805  576K  314K    3.44    2.93   50K  7744  8057   48K    8.84    5.97
c [distill] long cls tried: 14894/51811 cl-short:14878 lit-r:11406 T: 11.49 T-out: N T-r: 67.45%
c   luby     0   393  131K  143753  576K  314K    3.44    2.93   55K  6159 12488   48K   12.40    8.27
c   luby     0   420  139K  143753  576K  314K    3.44    2.93   58K  9959 11669   48K   22.46   14.68
c   luby     0   452  147K  143729  576K  314K    3.44    2.93   62K  8235 16689   49K   27.82   18.57
c   luby     0   458  155K  143719  576K  314K    3.44    2.93   67K  7809 16238   49K   38.15   25.51
c [distill] long cls tried: 19203/70742 cl-short:19172 lit-r:33773 T: 24.53 T-out: N T-r: 28.08%
c   luby     0   459  163K  143682  576K  314K    3.44    2.93   71K  6301   21K   49K   49.36   33.60
c recursive minimization cost OK: 10931Kcost/(% lits removed)
c [gauss] big_conflict/big_gaussnum:0.00 %
c [gauss] big_propagate/big_gaussnum:0.00 %
c --> Executing strategy token: handle-comps
c --> Executing strategy token: scc-vrepl
c [scc] new: 13 BP 0M T: 0.05
c --> Executing strategy token: cache-clean
c --> Executing strategy token: cache-tryboth
c --> Executing strategy token: sub-impl
c [impl sub] bin: 92378 T: 0.06 T-out: N w-visit: 290216
c --> Executing strategy token: intree-probe
c [scc] new: 15 BP 0M T: 0.03
c [vrep] vars 15 lits 416 rem-bin-cls 62 rem-long-cls 0 BP 1M T: 0.12
c [scc] new: 0 BP 0M T: 0.04
c [vrep] vars 0 lits 0 rem-bin-cls 0 rem-long-cls 0 BP 1M T: 0.16
c [intree] Set 0 vars hyper-added: 24695 trans-irred::50 trans-red::140 T: 17.24 T-out: Y T-r: -1.56%
c --> Executing strategy token: probe
c --> Executing strategy token: sub-str-cls-with-bin
c [distill] cache-based irred--  cl tried   575058 cl-sh  1536 cl-rem 2482 lit-rem   1536 T: 0.48 T-out: N
c [distill] cache-based   red--  cl tried   146523 cl-sh  1301 cl-rem  211 lit-rem   1705 T: 0.22 T-out: N
c --> Executing strategy token: distill-cls
c [distill] long cls tried: 8669/564465 cl-short:2980 lit-r:506 T: 3.24 T-out: Y T-r: -0.00%
c [distill] long useful: 5960/17338/1129230 lits-rem: 1012 0-depth-assigns: 4 T: 6.48 T-out: Y
c --> Executing strategy token: scc-vrepl
c [scc] new: 0 BP 0M T: 0.05
c --> Executing strategy token: sub-impl
c [impl sub] bin: 99 T: 0.05 T-out: N w-visit: 290216
c --> Executing strategy token: str-impl
c [impl str] lit bin: 1 (by stamp: 0) set-var: 1 T: 0.03 T-out: N T-r: 98.19% w-visit: 290216
c --> Executing strategy token: sub-impl
c [impl sub] bin: 0 T: 0.05 T-out: N w-visit: 290216
c --> Executing OCC strategy token(s): 'occ-backw-sub-str,occ-clean-implicit,occ-bve,occ-bva,occ-ternary-res,occ-xor,'
c [occ] mem usage for occur     40 MB
c [occ] mem usage for occur     20 MB
c Mem for watch alloc      : 1595        MB (0.00      %)
c Mem for watch array      : 6           MB (0.00      %)
c --> Executing OCC strategy token: occ-backw-sub-str
c [occ-backw-sub-str-long-w-bins] subs: 281 str: 194 tried: 2537761 0-depth ass: 0 T: 0.22 T-out: N T-r: 85.67%
c [occ-sub-long-w-long] rem cl: 4230 tried: 1324924/662462 (200.0%) T: 0.87 T-out: N T-r: 59.37%
c [occ-sub-str-long-w-long] sub: 168 str: 4772 tried: 1987386/662462 (300.0)  T: 1.82 T-out: N T-r: 12.75%
c [occ-sub-str-w-added-long]  sub: 0 str: 0 0-depth ass: 0 T: 0.00 T-out: N T-r: 99.92%
c --> Executing OCC strategy token: occ-clean-implicit
c --> Executing OCC strategy token: occ-bve
c [occ-empty-res] Empty resolvent elimed: 0 T: 0.08 T-out: N
c [occ-bve] iter v-elim 52
c cl_inc_rate=1.0, var_dec_rate=1.0 (grow=0)
c Reduced to 143610 vars, 789314 cls (grow=0)
c x n vars       : 143610
c  #try to eliminate:   143K
c  #var-elim        :     52
c  #T-o: N
c  #T-r: 99.80%
c  #T  : 1.01
c [occur] 0.62 is overhead
c [occur] link-in T: 0.62 cleanup T: 0.00
c --> Executing OCC strategy token: occ-bva
c [occ-bva] global numcalls: 1
c --> Executing OCC strategy token: occ-ternary-res
c --> Executing OCC strategy token: occ-xor
c [occ-xor] sort occur list T: 0.09
c [occ-xor] found  49756 avg sz 3.4 min sz  3 max sz  4 T: 0.71 T-out: N T-r: 99.41%
**CTRL-C**
sfiruch commented 4 years ago

As a point of reference: CaDiCaL solves this in ~1000s, CMS with default options or --xor=0 could not in 6000s.

msoos commented 4 years ago

Hey,

Ah, yeah. Well, Gaussian elimination doesn't always help -- only if XORs are really a very important part of the problem. Do you wanna send me this CNF, maybe I can debug?. Also CaDiCaL is differently optimized, sometimes it's faster, sometimes it's slower. On satisfiable instances, the difference is often due to random seeds of both solvers. Try them out, you'll see, you can get 2-3 orders of magnitude difference just by changing the seed for satisfiable instances. It's fun.

As for the O(n^2) issue -- yeah, good find! I have found this too, and it's been fixed in the development version. Unfortunately, I can't put it into public yet, because last time someone managed to download a new version of CryptoMiniSat, added nearly nothing to it, then published it as their own. So, no fun for anyone anymore!

However, if you send me the CNF, I promise to check and maybe I will even be able to send you some binary/give you access so you can check out our new version :) Could be nice!

sfiruch commented 4 years ago

[...] Do you wanna send me this CNF, maybe I can debug?. [...] However, if you send me the CNF, I promise to check and maybe I will even be able to send you some binary/give you access so you can check out our new version :) Could be nice!

Sure, it's here: https://github.com/msoos/cryptominisat/files/4005894/min5.zip

No need for sneak peeks. But let me know, if I can help by testing something (de@iru.ch).

msoos commented 4 years ago

Hi, so I looked at this, I am not sure I have the time to fix the speed issue here -- I am not sure that this is something that could be solved anyway, some things solve faster by some solvers than others. It can be quite random, in fact. Especially on satisfiable instances, where it's exceedingly hard to stabilize the time to solve. So, I have to close, because the underlying problem of xoring together being slow has been fixed already, and tuning the solver to this instance would be not the right thing to do, as there are many thousands where it also needs to perform well :( However, you are more than welcome to send this instance to the SAT competition! Then all SAT solvers will have to tune for your instance :)