Closed Heawen closed 3 years ago
smsharma1
commented
3 years ago Hi @Heawen, We need to change the hash range, the default value of the hash range is 64 with which we are not able to achieve the theoretical guarantees of probabilistic component caching. Please use the run_ganak.sh or take a look at the script for more details.
Thanks!
Heawen
commented
3 years ago Hi, thanks for your reply! I followed your advice, but after running for a few hours, the ganak output :
./run_ganak.sh chain21_4_mdad.cnf c Trying to run Ganak on chain21_4_mdad.cnf with timeout: 5000 c Ganak did NOT work
And there is no out.mc in the /scripts. I don't know what caused it to stop.
Here is the 'output' when ganak solving the cnf:
c Setting the timout to: 100000 c Outputting solution to console c GANAK version 1.0.0 c The value of hashrange is 64x1 c ganak GIT revision: 87440321d76d4ccf9d5a30ac9841a98d50eafa2a c ganak build env: CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES = | STATICCOMPILE = OFF | ONLY_SIMPLE = | Boost_FOUND = | ZLIB_FOUND = | ENABLE_TESTING = | ENABLE_ASSERTIONS = ON | MY_TARGETS = | compilation date time = May 11 2021 05:01:09 c Setting the timout to: 100000 c Solving chain21_4_mdad.cnf c variables (all/used/free): 416/416/0 c clauses (all/long/binary/unit): 1347/977/366/4 c Sampling set not present! So doing total model counting. c c Preprocessing .. c DONE c variables (all/used/free): 398/398/0 c clauses (all/long/binary/unit): 1272/921/351/0 c Maximum cache size: 2000 MB c c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c Max decision level :25
Waiting for your reply.
smsharma1
commented
3 years ago Hey @Heawen, It looks like the example cnf is difficult to solve for ganak. If you look at the run_ganak.sh script we are using the timeout of 5000 secs (tout_ganak=5000) and that's why in your case ganak stopped after 5000 secs without any output.
You can try increasing this value to 10000/15000 secs.
Heawen
commented
3 years ago Thanks a lot!
Heawen
commented
3 years ago Hi, @smsharma1 I changed the timeout from 5000 secs to 1000000 secs ( tout_ganak=1000000) in the run_ganak.sh script. But ganak stopped again after almost 27 hours( 100000 secs), and the output is:
./run_ganak.sh chain21_4_mdad.cnf c Trying to run Ganak on chain21_4_mdad.cnf with timeout: 1000000 c Trying to run Ganak on chain21_4_mdad.cnf with timeout: 1000000 c Ganak did NOT work
Before it stopped, the hashrange changed to 2 . In the output file:
c Setting the timout to: 100000 c Outputting solution to console c GANAK version 1.0.0 c The value of hashrange is 64x2 c ganak GIT revision: 87440321d76d4ccf9d5a30ac9841a98d50eafa2a c ganak build env: CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES = | STATICCOMPILE = OFF | ONLY_SIMPLE = | Boost_FOUND = | ZLIB_FOUND = | ENABLE_TESTING = | ENABLE_ASSERTIONS = ON | MY_TARGETS = | compilation date time = May 11 2021 05:01:09 c Setting the timout to: 100000 c Solving chain21_4_mdad.cnf c variables (all/used/free): 416/416/0 c clauses (all/long/binary/unit): 1347/977/366/4 c Sampling set not present! So doing total model counting. c c Preprocessing .. c DONE c variables (all/used/free): 398/398/0 c clauses (all/long/binary/unit): 1272/921/351/0 c Maximum cache size: 2000 MB
It may take several days to find the exact solution number for ganak, and before that what should I do to keep ganak running ?
Can I set a large hashrange before I run ganak? Will it help to shorten the solution time?
Hi, I met some problem when the ganak solved cnf. Can you help me check out?
''' ./ganak chain21_4_mdad.cnf
c Setting the timout to: 100000 c Outputting solution to console c GANAK version 1.0.0 c ganak GIT revision: GIT-notfound c ganak build env: CMAKE_CXX_COMPILER = /usr/bin/c++ | CMAKE_CXX_FLAGS = -mtune=native -Wall -Wextra -Wunused -Wsign-compare -fno-omit-frame-pointer -Wtype-limits -Wuninitialized -Wno-deprecated -Wstrict-aliasing -Wpointer-arith -Wpointer-arith -Wformat-nonliteral -Winit-self -Wparentheses -Wunreachable-code -ggdb3 | COMPILE_DEFINES = | STATICCOMPILE = OFF | ONLY_SIMPLE = | Boost_FOUND = | ZLIB_FOUND = | ENABLE_TESTING = | ENABLE_ASSERTIONS = ON | MY_TARGETS = | compilation date time = May 10 2021 11:16:22 c Setting the timout to: 100000 c Solving chain21_4_mdad.cnf c variables (all/used/free): 416/416/0 c clauses (all/long/binary/unit): 1347/977/366/4 c Sampling set not present! So doing total model counting. c c Preprocessing .. c DONE c variables (all/used/free): 398/398/0 c clauses (all/long/binary/unit): 1272/922/350/0 c Maximum cache size: 9376 MB c c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c We have solved halfed c Max decision level :25 c Max decision level :50 c Cache full!! ERROR: We need to change the hash range (-1) ''''
Waiting for your reply. Thanks