Allow memory to grow larger than 4GB per thread

[msoos]

Currently, long-running instances die with memory overload.

[anma77]

Dear Mate, thank you for the fast reaction. Because I let the jobs run in verb=4 I wonder why there was no memory overload message in the log-files. But if you say it, it must be so. It is a pity because I really have very much memory on my system. For cryptographic purposes termination is important. Big instances should be able to run longer. Thank you very much!

[BA-Bartsch]

+1
Started an instance with 8 threads and crashed when ram usage reached approx. 8GB (system had 64GB)

Errormessage:
ERROR: memory manager can't handle the load size: 1073737728 needed: 13444 newcapacity: 1073741823
terminate called after throwing an instance of 'std::bad_alloc'
what(): std::bad_alloc

Benjamin

[anma77]

I can imagine that the duration of the execution, before the solver stops, varies with the magnitude of the problem but also with the switches which manipulate the learned clauses. The longer it runs the bigger the data base and from a point and on the matter becomes not manageable. I was surprised to read in an older paper of Henry Kautz & Bart Selman ("The State of SAT") about solvers terminating successfully after 25 days! I wonder if other modern solvers have a memory limitation like CMS

[msoos]

All the serious ones do. The State of SAT was written in 2007. The optimisation that restricts to 32b offsets is a new one. MiniSat, Glucose, lingeling, etc. all have it. However, it is true that current CryptoMiniSat hoards a bit too many learnt clauses, hence it terminates earlier than other solvers. But they all would. Again, I am working on it, but 2007 is not 2017 :)

[anma77]

Mate you mean that what was solved in 25 days in the year 2007, is now solvable is some minutes ? :-)
Nichts für Ungut! Best regards!

[msoos]

:) Unfortunately, no. But what was true then is not necessarily true now, because the incentives for SAT solver writers are not to solve issues that take 25 days to solve, but to solve issues that take at most 3-4h to solve. A new idea came around since 2007 that restricts the maximum time, but lowers the time to solve when under 4h. So everybody is using it. If the SAT competition was set up such that a solver has to be able to run for 25 days, then nobody would use this idea, because it would prevent the people from winning. So, it's a double-edged sword.

Again, I will fix it, there is no need to push :)

[anma77]

I didn't mean to push Mate! But this limitation doesn't fit the cryptography-business ;-)
And besides, your solver is specialized for cryptographic problems! (Now I push!)
Best wishes and thanks!

[BA-Bartsch]

Running the same instance in 8 separate tread leads to longer execution times (since 26h no error). One thread uses currently 2GB ram slowly increasing, reaching the 4GB limit in approx 2 days. This observation suggests, that running 8 threads in parallel leads to 8 times as fast clause collection (somehow logic), therefore the 4GB limit is reached 8 times faster.

A workaround could be, that a thread deletes clauses which came from others threads more aggressively.

[anma77]

Hello BA-Bartsch. I am not sure that clause deleting out of memory considerations would be a useful strategy for all cases. It could be that useful clauses get lost in this way. And maybe the relation of the number of threads to the fastness of reaching the memory limit is also not "linear". I take 48 threads. Some jobs run for fast 5 days before they die out, other run even a bit longer. The jobs which I let run with 35 threads do not manage to survive longer though. This is why I doubt the direct proportionality suggested above...

[BA-Bartsch]

If you compare 48 threads to 35 threads then the "linearity" would only apply if the pc has true 48 cores (or HT), otherwise the 48 threads are slowed down.

Nevertheless I really love your program and I thank you very much for programming/debugging it!

[msoos]

Actually, the whole diff to add this feature is a hell of a lot less than the number of lines written in this issue :) I'm about to push it. Let's just stick to that :)

[anma77]

Mate, this is a Word! Wishing you both a nice evening!

[msoos]

It's now been added. You can test this by:

• compiling with cmake option "-DLARGEMEM=ON"
• uncommenting # clause_alloc_test in test/CMakeLists.txt
• running the compiled clause_alloc_test.cpp, usually under build/tests/clause_alloc_test

It should print that the memory get consolidated correctly even after e.g. 10GB of clause memory usage. Note that the test is currently not enabled, and the "test" it performs is rather stupid, it just checks that the solve() doesn't crash. Which it would if the consolidation made a mistake. Note that I cannot run this test, as I only have 12GB of memory. I'd need about twice that to test this. Note that this may start using your swap and "crash" (make it unusable) your computer. So, thread carefully. Make sure you have a lot of RAM, say, 64GB.

Feedback would be appreciated, especially the output of that executable.

PS: I can go up to:

c [mem] Consolidated memory  old size  2746MB new size 2746MB bits of offset:28.35 T: 1.15

which means 2.7GB of memory usage, offset is only at 29b usage. We need >32b to correctly test this (i.e. 16x more RAM usage), so you need a lot of RAM, possibly over 100GB (as it needs to grab 2x what it needs + there is overhead from other parts of the solver that affect the overall memory usage -- at 2.7GB of clause usage it was using over 4GB of real RAM + on consolidation it was using 8GB, so ~16x8GB is what is needed for a proper test. You might need to adjust the max number of clauses, currently set to uint64_t num = 10ULL*1000ULL*1000ULL; i.e. 10M)

[msoos]

I see that this thread was very busy, which is great! I spent a full 4h (i.e. my evening) on this. It'd be nice one of you could take the ~10 minutes to do the test, as I cannot perform it :S Thanks in advance!

[BA-Bartsch]

how do I compile clause_alloc_test.cpp?
"cmake ." in the "test" directory leads to following error:

CMake Error at CMakeLists.txt:17 (message):
  Could not find 'lit' tool.  You need to install it by e.g.  'pip install
  lit' If it's already installed, set LIT_TOOL to the full path for lit


CMake Warning (dev) in CMakeLists.txt:
  No cmake_minimum_required command is present.  A line of code such as

    cmake_minimum_required(VERSION 3.5)

  should be added at the top of the file.  The version specified may be lower
  if you wish to support older CMake versions for this project.  For more
  information run "cmake --help-policy CMP0000".
This warning is for project developers.  Use -Wno-dev to suppress it.

[anma77]

good morning to all! THANK YOU Mate! I have 256GB real RAM, so that is no problem! But I first have to compile the new version and send the jobs. I will be back soon. And again: Many thanks !

[BA-Bartsch]

I did not manage to compile the cpp-test-file. So I started one of my calculations with 8 threads on a system with 64GB ram. Here is a diagram which shows "Time vs. Ram". Its still running, so I would call it a success!
Benjamin

[msoos]

Well, it says "pip install lit" is needed, so maybe that would help? :) Install pip then install lit with pip :)

…

On 3 May 2017 05:51, "BA-Bartsch" ***@***.***> wrote: how do I compile clause_alloc_test.cpp? "cmake ." in the "test" directory leads to following error: CMake Error at CMakeLists.txt:17 (message): Could not find 'lit' tool. You need to install it by e.g. 'pip install lit' If it's already installed, set LIT_TOOL to the full path for lit CMake Warning (dev) in CMakeLists.txt: No cmake_minimum_required command is present. A line of code such as cmake_minimum_required(VERSION 3.5) should be added at the top of the file. The version specified may be lower if you wish to support older CMake versions for this project. For more information run "cmake --help-policy CMP0000". This warning is for project developers. Use -Wno-dev to suppress it. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#389 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABReOTg2w9dw3agPigKI2xJuFcFbCqbNks5r2AeygaJpZM4M3yXW> .

[msoos]

Since this is a per-thread limit, running with many threads will only limit us in terms of testing. I *strongly* recommend testing with only *one* thread so you can reach e. g. 16 Gigs with one thread. Then we can be more sure it's fixed :)

…

On 4 May 2017 08:35, "BA-Bartsch" ***@***.***> wrote: I did not manage to compile the cpp-file. So I started one of my calculations with 8 threads on a system with 64GB ram. Here is a diagram which shows "Time vs. Ram". Benjamin [image: time_vs_ram] <https://cloud.githubusercontent.com/assets/28258470/25694074/019a7ae6-30ad-11e7-9a24-f954cec94c29.png> — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#389 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABReOexP-0ylGahaYkavcus1HFHyODQSks5r2X_WgaJpZM4M3yXW> .

[BA-Bartsch]

I have no idea how to install them. I am so bad at linux, I can only copy-paste things or use 1-click-links. I managed to compile cryptominisat after more than 2 hours trial and error and I saved it for the future:

sudo apt-get install build-essential cmake
sudo apt-get install libboost-program-options-dev libm4ri-dev libsqlite3-dev

tar xzvf cryptominisat-version.tar.gz
cd cryptominisat-version
cmake -DLARGEMEM=ON -DUSE_GAUSS=ON .
make

sudo make install
sudo ldconfig

could you provide me a "sudo apt-get install ...." line to install pip / lit.

sudo apt-get install pip
sudo apt-get install lit 

did not work.

[BA-Bartsch]

ohh there was the hint:
NOTE: if adding the 'gtest' subdirectory fails, you need to issue 'git submodule init' and 'git submodule update'

ok lets run:
git submodule init

it tells me in german that git is not installed:
Die Anwendung »git« ist momentan nicht installiert. Sie können sie durch folgende Eingabe installieren: sudo apt install git

ok lets run:
sudo apt install git

seems to be installed, ok lets run again:
git submodule init

and it tells me:
fatal: Not a git repository (or any of the parent directories): .git

now I am stuck

[msoos]

@BA-Bartsch I have now added instructions how to build this from the ground up in the README. You need to first of all delete your cryptominisat -- you are probably using the tarball/zip, that's not good. Now you need to do the following:

$ sudo apt-get install build-essential cmake
$ sudo apt-get install libboost-program-options-dev libm4ri-dev libsqlite3-dev
$ sudo apt-get install git python-pip python-setuptools python-dev
$ sudo pip install pip
$ git clone https://github.com/msoos/cryptominisat.git
$ cd cryptominisat
$ git submodule update --init
$ mkdir build && cd build
$ cmake -DLARGEMEM=ON -DENABLE_TESTING=ON ..
$ make -j4
$ make test
$ sudo make install
$ sudo ldconfig

On top of that, you need to enable the test as per my instructions above, removing the "#" from the CMakeLists.txt indicated before running the "cmake" command. But in all honesty, you are probably better off not doing testing in case you don't have a software developer background. It's a bit tricky :)

[BA-Bartsch]

Hey, everything worked, thank you!

After "make test":
Test project /home/user17/Schreibtisch/CM_TEST/cryptominisat/build
      Start  1: readme_test
 1/22 Test  #1: readme_test .......................   Passed    0.02 sec
      Start  2: c_test
 2/22 Test  #2: c_test ............................   Passed    0.01 sec
      Start  3: multisol_test
 3/22 Test  #3: multisol_test .....................   Passed    0.02 sec
      Start  4: clause_alloc_test
 4/22 Test  #4: clause_alloc_test .................   Passed  137.21 sec
      Start  5: basic_test
 5/22 Test  #5: basic_test ........................   Passed    0.67 sec
      Start  6: assump_test
 6/22 Test  #6: assump_test .......................   Passed    0.01 sec
      Start  7: heap_test
 7/22 Test  #7: heap_test .........................   Passed    0.00 sec
      Start  8: clause_test
 8/22 Test  #8: clause_test .......................   Passed    0.00 sec
      Start  9: stp_test
 9/22 Test  #9: stp_test ..........................   Passed    0.01 sec
      Start 10: scc_test
10/22 Test #10: scc_test ..........................   Passed    0.01 sec
      Start 11: vrepl_test
11/22 Test #11: vrepl_test ........................   Passed    0.00 sec
      Start 12: clause_cleaner_test
12/22 Test #12: clause_cleaner_test ...............   Passed    0.00 sec
      Start 13: probe_test
13/22 Test #13: probe_test ........................   Passed    0.01 sec
      Start 14: distiller_all_with_all_test
14/22 Test #14: distiller_all_with_all_test .......   Passed    0.00 sec
      Start 15: distill_long_with_implicit_test
15/22 Test #15: distill_long_with_implicit_test ...   Passed    0.00 sec
      Start 16: subsume_impl_test
16/22 Test #16: subsume_impl_test .................   Passed    0.00 sec
      Start 17: comp_find_test
17/22 Test #17: comp_find_test ....................   Passed    0.00 sec
      Start 18: intree_test
18/22 Test #18: intree_test .......................   Passed    0.00 sec
      Start 19: xorfinder_test
19/22 Test #19: xorfinder_test ....................   Passed    0.01 sec
      Start 20: comphandler_test
20/22 Test #20: comphandler_test ..................   Passed    0.00 sec
      Start 21: CNF
21/22 Test #21: CNF ...............................   Passed    0.28 sec
      Start 22: verifier_test
22/22 Test #22: verifier_test .....................   Passed    0.03 sec

100% tests passed, 0 tests failed out of 22

Total Test time (real) = 138.33 sec

and explicit calling "./clause_alloc_test"

[==========] Running 1 test from 1 test case.
[----------] Global test environment set-up.
[----------] 1 test from clause_allocator
[ RUN      ] clause_allocator.add_1
Added 0M T:0
c [mem] Consolidated memory  old size    440B new size   440B bits of offset:5.78 T: 0.00
Added 0M T:1.74
c [mem] Consolidated memory  old size   119MB new size  119MB bits of offset:23.83 T: 0.06
Added 0M T:3.48
c [mem] Consolidated memory  old size   238MB new size  238MB bits of offset:24.83 T: 0.09
Added 0M T:5.25
c [mem] Consolidated memory  old size   358MB new size  358MB bits of offset:25.42 T: 0.11
Added 0M T:7.06
c [mem] Consolidated memory  old size   477MB new size  477MB bits of offset:25.83 T: 0.17
Added 0M T:8.92
c [mem] Consolidated memory  old size   596MB new size  596MB bits of offset:26.15 T: 0.20
Added 0M T:10.80
c [mem] Consolidated memory  old size   716MB new size  716MB bits of offset:26.42 T: 0.28
Added 0M T:12.77
c [mem] Consolidated memory  old size   835MB new size  835MB bits of offset:26.64 T: 0.27
Added 0M T:14.73
c [mem] Consolidated memory  old size   955MB new size  955MB bits of offset:26.83 T: 0.37
Added 0M T:16.79
c [mem] Consolidated memory  old size  1074MB new size 1074MB bits of offset:27.00 T: 0.34
Added 1M T:18.82
c [mem] Consolidated memory  old size  1193MB new size 1193MB bits of offset:27.15 T: 0.45
Added 1M T:20.96
c [mem] Consolidated memory  old size  1313MB new size 1313MB bits of offset:27.29 T: 0.40
Added 1M T:23.08
c [mem] Consolidated memory  old size  1432MB new size 1432MB bits of offset:27.42 T: 0.58
Added 1M T:25.34
c [mem] Consolidated memory  old size  1552MB new size 1552MB bits of offset:27.53 T: 0.51
Added 1M T:27.56
c [mem] Consolidated memory  old size  1671MB new size 1671MB bits of offset:27.64 T: 0.67
Added 1M T:29.92
c [mem] Consolidated memory  old size  1790MB new size 1790MB bits of offset:27.74 T: 0.56
Added 1M T:32.18
c [mem] Consolidated memory  old size  1910MB new size 1910MB bits of offset:27.83 T: 0.76
Added 1M T:34.64
c [mem] Consolidated memory  old size  2029MB new size 2029MB bits of offset:27.92 T: 0.58
Added 1M T:36.91
c [mem] Consolidated memory  old size  2149MB new size 2149MB bits of offset:28.00 T: 0.89
Added 1M T:39.48
c [mem] Consolidated memory  old size  2268MB new size 2268MB bits of offset:28.08 T: 0.69
Added 2M T:41.86
c [mem] Consolidated memory  old size  2388MB new size 2388MB bits of offset:28.15 T: 0.93
Added 2M T:44.48
c [mem] Consolidated memory  old size  2507MB new size 2507MB bits of offset:28.22 T: 0.82
Added 2M T:46.98
c [mem] Consolidated memory  old size  2626MB new size 2626MB bits of offset:28.29 T: 1.04
Added 2M T:49.71
c [mem] Consolidated memory  old size  2746MB new size 2746MB bits of offset:28.35 T: 0.85
Added 2M T:52.25
c [mem] Consolidated memory  old size  2865MB new size 2865MB bits of offset:28.42 T: 1.16
Added 2M T:55.10
c [mem] Consolidated memory  old size  2984MB new size 2984MB bits of offset:28.48 T: 0.94
Added 2M T:57.72
c [mem] Consolidated memory  old size  3104MB new size 3104MB bits of offset:28.53 T: 1.29
Added 2M T:60.71
c [mem] Consolidated memory  old size  3223MB new size 3223MB bits of offset:28.59 T: 0.97
Added 2M T:63.37
c [mem] Consolidated memory  old size  3342MB new size 3342MB bits of offset:28.64 T: 1.37
Added 2M T:66.44
c [mem] Consolidated memory  old size  3462MB new size 3462MB bits of offset:28.69 T: 1.05
Added 3M T:69.18
c [mem] Consolidated memory  old size  3581MB new size 3581MB bits of offset:28.74 T: 1.50
Added 3M T:72.38
c [mem] Consolidated memory  old size  3701MB new size 3701MB bits of offset:28.79 T: 1.13
Added 3M T:75.20
c [mem] Consolidated memory  old size  3820MB new size 3820MB bits of offset:28.83 T: 1.61
Added 3M T:78.52
c [mem] Consolidated memory  old size  3939MB new size 3939MB bits of offset:28.88 T: 1.20
c [mem] Consolidated memory  old size  3979MB new size 3979MB bits of offset:28.89 T: 1.62
c --> Executing strategy token: sub-impl
c [impl sub] bin: 0 tri: 0 (stamp: 0, cache: 0) T: 0.09 T-out: Y w-visit: 62074
c --> Executing strategy token: scc-vrepl
c --> Executing OCC strategy token(s): 'occ-backw-sub-str,occ-clean-implicit,occ-bve,'
c [clean] T: 1.7640 s
c [scc] new: 0 BP 4M T: 0.02
c --> Executing strategy token: sub-str-cls-with-bin
c [clean] T: 1.7600 s
c [distill-with-bin-ext] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0
c [distill-with-bin-ext] bin-based lit-rem: 0 cl-sub: 0
c [distill-with-bin-ext] cache-based lit-rem: 0 cl-sub: 0
c [distill-with-bin-ext] T: 0.28 T-out: Y T-r: -0.00%
c [distill-with-bin-ext] stamp-based lit-rem: 0 inv-lit-rem: 0 stamp-cl-rem: 0
c [distill-with-bin-ext] bin-based lit-rem: 0 cl-sub: 0
c [distill-with-bin-ext] cache-based lit-rem: 0 cl-sub: 0
c [distill-with-bin-ext] T: 0.24 T-out: Y T-r: -0.14%
c [distill] cache-based irred--  cl tried     2056 cl-sh     0 cl-rem    0 lit-rem      0 T: 0.52 T-out: Y
c [distill] cache-based   red--  cl tried        0 cl-sh     0 cl-rem    0 lit-rem      0 T: 0.00 T-out: N
c [consolidate] T: 0.00
c [extend] Extended 0 var-elim clauses
[       OK ] clause_allocator.add_1 (94117 ms)
[----------] 1 test from clause_allocator (94117 ms total)

[----------] Global test environment tear-down
[==========] 1 test from 1 test case ran. (94117 ms total)
[  PASSED  ] 1 test.

But should'nt it try to allocate more ram?
Benjamin

[msoos]

I'll close this now, it seems fixed. Thanks everyone!