search

msoos / cryptominisat

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

Displayed time (of some parts) not complete? #706

Closed capiman closed 1 year ago

capiman commented 1 year ago

I think measurements are not complete (parts taking time are not displayed?) (Attention: Only a test run. I know it is no normal use case. System does a lot swapping. Hope it is not due to swapping. This run takes 256 GByte of memory (but only 64 GByte real memory), so perhaps something seen is more extreme than in regular runs.

... Dez 28 12:14:15 c Number of solutions found until now: 2389270 Dez 28 12:14:15 c rst geom ibes vs 2389640 2585K 20562 43M 25M 1143.48 722.14 2298 735 17357 28 107.08 106.93 Dez 28 12:14:15 s SATISFIABLE Dez 28 12:14:15 c Not printing satisfying assignment. Use the '--printsol 1' option for that Dez 28 12:14:15 c Number of solutions found until now: 2389271 Dez 28 12:14:15 c rst geom ibes vs 2389641 2585K 20562 43M 25M 1143.48 722.14 2298 735 17359 28 107.07 106.92 Dez 28 12:14:15 s SATISFIABLE Dez 28 12:14:15 c Not printing satisfying assignment. Use the '--printsol 1' option for that Dez 28 12:14:15 c Number of solutions found until now: 2389272 Dez 28 12:14:15 c [gauss] XOR-encoding clauses are not detached, so no need to reattach them. Dez 28 12:29:03 c [scc] new: 0 BP 34M T: 0.33 Dez 28 12:52:11 c [vrep] vars 0 lits 0 rem-bin-cls 0 rem-long-cls 0 BP 129M T: 92.65 Dez 28 12:52:11 c [intree] too expensive or depth exceeded during SCC: aborting Dez 28 12:52:11 c [find&init matx] performing matrix init Dez 28 12:52:11 c [gauss] XOR-encoding clauses are not detached, so no need to reattach them. Dez 28 12:52:11 c [matrix] unused xors from cleaning: 0 Dez 28 12:52:17 c rst geom ibes vs 2389642 2585K 20562 43M 25M 1143.48 722.14 2298 735 17361 28 107.06 106.92 Dez 28 12:52:17 s SATISFIABLE Dez 28 12:52:17 c Not printing satisfying assignment. Use the '--printsol 1' option for that Dez 28 12:52:17 c Number of solutions found until now: 2389273 Dez 28 12:52:17 c rst geom ibes vs 2389643 2585K 20562 43M 25M 1143.48 722.14 2298 735 17361 28 107.06 106.92 Dez 28 12:52:17 s SATISFIABLE Dez 28 12:52:17 c Not printing satisfying assignment. Use the '--printsol 1' option for that ...

Info:

c BreakID not compiled in, disabling c CryptoMiniSat version 5.11.7 c CMS Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file c CMS SHA revision fdcd5835f1f959b55d1c9a5743bf157dda6db652 c CMS is MIT licensed c Using VMTF code by Armin Biere from CaDiCaL c Using Yalsat by Armin Biere, see Balint et al. Improving implementation of SLS solvers [...], SAT'14 c Using WalkSAT by Henry Kautz, see Kautz and Selman Pushing the envelope: planning, propositional logic, and stochastic search, AAAI'96, 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 Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]' c by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015 c CMS compilation env CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -fvisibility=hidden -Wall -Wextra -Wunused -Wsign-compare -fno-om it-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-se lf -Wparentheses -Wunreachable-code -g -Wno-class-memaccess -mpopcnt -msse4.2 -ggdb3 -Wlogical-op -Wrestrict -Wnull-dereference -Wdouble-promo tion -Wshadow -Wformat=2 -Wextra-semi -pedantic | COMPILE_DEFINES = -DLARGE_OFFSETS -DRDB0_ONLY_FEATURES -DBOOST_TEST_DYN_LINK -DUSE_ZLIB -DY ALSAT_FPU | STATICCOMPILE = OFF | ONLY_SIMPLE = OFF | Boost_FOUND = TRUE | STATS = OFF | SQLITE3_FOUND = | ZLIB_FOUND = TRUE | VALGRIND_FOUND = | ENABLE_TESTING = OFF | M4RI_FOUND = | NOM4RI = ON | SLOW_DEBUG = OFF | ENABLE_ASSERTIONS = ON | PYTHON_EXECUTABLE = | PYTHON_LIBRARY = | PYTHON_INCLUDE_DIRS = | MY_TARGETS = | LARGEMEM = ON | LIMITMEM = OFF | BREAKID_LIBRARIES = | BREAKID-VER = . | BOSPHORUS_LIBRARIES = | BOSPH-VER = . | compilation date time = Dec 26 2022 20:23:10 c CMS compiled with gcc version 11.3.0 c Executed with command line: ../cryptominisat-20221226/build/cryptominisat5 --distill=0 --distillbin=0 --sls=0 --bva=0 --renumber=0 --slsmaxm em=50000 --intreemaxm=120000 --maxsol=5000000 --transred=0 --printsol=0 --dumpres=... --input=...

msoos commented 1 year ago

Hi, this is a known issue and I don't intend to fix it. It's extremely complicated to fix and I don't have the time. I am expecting this to be hundreds of lines of code to fix, if not a thousand or more. I can't do that for such a minor issue. You can always run it under perf record --call-graph=dwarf ./cryptominisat5 [STUFF] and then use perf report to see what took how much time. It will be both more accurate and way better than any timing I could do.