srogatch
commented
2 months ago This is the output in 3.4.0:
c----------[ Banner ]------------------------------------------------------------------------
c
c ██████╗░░█████╗░██████╗░░█████╗░███████╗██████╗░░█████╗░░██████╗████████╗
c ██╔══██╗██╔══██╗██╔══██╗██╔══██╗██╔════╝██╔══██╗██╔══██╗██╔════╝╚══██╔══╝
c ██████╔╝███████║██████╔╝███████║█████╗░░██████╔╝██║░░██║╚█████╗░░░░██║░░░
c ██╔═══╝░██╔══██║██╔══██╗██╔══██║██╔══╝░░██╔══██╗██║░░██║░╚═══██╗░░░██║░░░
c ██║░░░░░██║░░██║██║░░██║██║░░██║██║░░░░░██║░░██║╚█████╔╝██████╔╝░░░██║░░░
c ╚═╝░░░░░╚═╝░░╚═╝╚═╝░░╚═╝╚═╝░░╚═╝╚═╝░░░░░╚═╝░░╚═╝░╚════╝░╚═════╝░░░░╚═╝░░░
c Copyright© Muhammad Osama Mahmoud v3.4.0
c
c----------[ Build ]-------------------------------------------------------------------------
c Available CPU: AMD Ryzen Threadripper 3990X 64-Core Processor
c Available system memory: 251 GB
c Built on linux sarge-pc2020 6.8.0-41-generic x86_64 at wto, 17 wrz 2024, 19:02:47 +03
c using g++ (Ubuntu 13.2.0-23ubuntu4) 13.2.0 + nvcc 12.6.68 (release mode)
c Forced FPU to use double precision
c Available GPU: 4 x NVIDIA RTX 6000 Ada Generation @ 2.50GHz (compute cap: 8.9)
WARNING - cannot map to cores/SM due to unknown SM
c Available GPU Multiprocessors: 142 MPs (unknown cores/MP)
c Available Global memory: 47 GB
c----------[ Parser ]------------------------------------------------------------------------
c Parsing CNF file "../../../../data/bc_2024-09-17.cnf" (size: 79 MB)
c Found header 679480 3477812
c Read 679480 Variables, 3477812 Clauses, and 10460189 Literals in 0.52 seconds
c found 2936 units, 280086 binaries, 2887012 ternaries, 307778 larger
c maximum clause size: 97
c----------[ Search ]------------------------------------------------------------------------
c ORG Conflicts Restarts Learnt V(%) C(%)
c V C L C L L/C
c--------------------------------------------------------------------------------------------
c - 672481 3470560 10443603 0 0 0 0 0 98% 99%
c s 528778 0 0 0 0 0 0 0 77% 0%
c----------[ Result ]------------------------------------------------------------------------
c
s SATISFIABLE
c
c----------[ Statistics ]--------------------------------------------------------------------
c Simplifier Report
c Simplifier time : 0.000 sec
c Device memory : 494.534 MB
c Sigmifications : 1
c Forced units : 0
c Removed variables : 143703
c Removed clauses : 3470560
c Removed literals : 0
c Removed redundancies : 0
c
c Solver Report
c Solver time : 0.389 sec
c System memory : 405.656 MB
c Formula : ../../../../data/bc_2024-09-17.cnf
c Size : 79.771 MB
c Units : 2936
c Binaries : 280086
c Ternaries : 2887012
c Larger : 307778
c Max clause size : 97
c C2V ratio : 5.114
c Autarky calls : 0
c Removed variables : 0
c Backtracks : 0
c Chronological : 0
c Non-Chronological : 0
c Trail reuses : 0
c Conflicts : 0
c OTF strengthened : 0
c OTF subsumed : 0
c Learnt OTF subsumes : 0
c Learnt OTF subsumed : 0
c Learnt units : 0
c Learnt literals : 0
c Deduplications : 0
c Hyper unaries : 0
c Duplicated binaries : 0
c Decompositions : 0
c SCCs : 0
c Hyper unaries : 0
c Removed variables : 0
c Removed clauses : 0
c Hyper binary resolves : 0
c Added binaries : 0
c Hyper ternary resolves : 0
c Added binaries : 0
c Added ternaries : 0
c Subsumed ternaries : 0
c Reduces : 0
c Restarts : 0
c Stable restarts : 0
c Stable modes : 0
c Unstable modes : 0
c Rephases : 0
c Walk : 0
c Recyclings : 0
c Soft : 0
c Hard : 0
c Probes calls : 0
c Rounds : 0
c Probed : 0
c Failed : 0
c Ticks : 0
c Transitive calls : 0
c Probed : 0
c Failed : 0
c Transitives : 0
c Ticks : 0
c Subsume calls : 0
c Checks : 0
c Subsumed : 0
c Strengthened : 0
c Search decisions : 0
c Assumptions : 0
c Propagations : 6999
c Ticks : 1184
c Mappings : 0
c MDM calls : 0
c Walks : 0
c VMTF uses : 0
c VSIDS uses : 0
c All decisions : 0
c Last-made decisions : 0
c Vivification checks : 0
c Vivified : 0
c Walk calls : 0
c Checks : 0
c Minimum : 0
c Flipped : 0
c Improved : 0
c
c----------[ Exit ]--------------------------------------------------------------------------
ERROR - cannot (de)allocate new memory block via the cache allocator
muhos
I'm getting this error for a formula of ~80 MB. Why is that and what does it mean?