When timeout set: > 100000 sec, ganak stopped at 100000 sec

[Heawen]

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?

Originally posted by @Heawen in https://github.com/meelgroup/ganak/issues/12#issuecomment-840259701

[smsharma1]

Hi @Heawen, Yes, let's increase the hash range to 4 and try running ganak with a very large timeout value. Looks like the example you are running is very hard for ganak to solve.

[Heawen]

Thanks for your reply! :) I changed the run_ganak.sh file : ./run_ganak.sh

tout_arjun=100 tout_ganak=5000000 maximum_component_cache_size=2000 input_file=$1 rm -f independent rm -f out rm -f newfile rm -f input rm -rf *.out run_ganak=true hash_range=4

Here is the output file:

c Setting the timout to: 100000 c Outputting solution to console c GANAK version 1.0.0 c time bound set to 5000000s c The value of hashrange is 64x4 c ganak GIT revision: 87440321d76d4ccf9d5a30ac9841a98d50eafa2a c ganak build env: ..... c Setting the timout to: 5000000 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.

Is this big enough?

[smsharma1]

The changed parameters are looking good to me. We don't know upfront how difficult the problem is so we can not predict if the set parameters will be sufficient, but for the starting point, the above values are looking good to me.