Not understand the output of sharpSAT

[Heawen]

Hello! Your work helps me a lot!

I'm new to the #SAT problem, and I don't understand the output of sharpSAT.
In my case, why the "cache miss rate" is not 100% and what's the impact of that?
It's necessary for me to know whether the output number is the exact number of solutions.

The output of sharpSAT:
"""
variables (total / active / free) 218/218/0
clauses (removed) 804 (24)
decisions 312225169
conflicts 9
conflict clauses (all/bin/unit) 119/1/0

failed literals found by implicit BCP 109
implicit BCP miss rate 100%
bytes cache size 254763328
bytes cache (overall) 88446113808
bytes cache (infra / comps) 29508704/225254624
bytes pure comp data (curr) 172331424
bytes pure comp data (overall) 68434193712
bytes cache with sysoverh (curr) 276516640
bytes cache with sysoverh (overall) 107816675392
cache (stores / hits) 1452254/1333240957
cache miss rate 18.9749%
avg. variable count (stores / hits) 52.9823/20.1939

solutions
1511157274518286468382720
END

time: 8630.13s
"""
I'm looking forward to your reply.

[VincentDerk]

The cache miss rate does not relate to the correctness of your solution. It instead tells you how often it was able to use the cache to avoid computations. The closer the cache miss rate is to 0% the better it was able to exploit the caching. If your cache miss rate is 100%, the cache was unable to reduce the number of components to solve.

[Heawen]

Thanks for your response! :)
So the sharpSAT can always find the exact number of sulotions, regardless of the running time.
And I have a question about the running time. Is there any method to estimate the running time? I have got several instances which are similar in scales (the number of varibles, clause) but cost different time to get the output.

[VincentDerk]

So the sharpSAT can always find the exact number of sulotions, regardless of the running time.

sharpSAT is an exact model counter so it will always give you the exact number of solutions (ignoring unknown potential bugs or hard problems that make it run forever/out of memory).

And I have a question about the running time. Is there any method to estimate the running time?

I personally haven't looked too much into that, perhaps someone else can answer you better. I am aware of for example this paper https://arxiv.org/pdf/2007.10400.pdf where they analyse the impact of No variables, clause length, No clauses / No variables,... on the hardness of problems. You might be able to find related work.

In general, the run time is influenced by the CNF structure, and by the heuristics in the model counter (e.g. the variable selection heuristic).

[Heawen]

Thanks again ! :)

[Heawen]

Another question:
When the running time exceeds 100000s, SharpSAT stopped automatically. Can I cancel it ?
'''''
time elapsed: 99979s
ts 1048576 1048575
coll 3468
ts 1048576 1048575
coll 2977
ts 1048576 1048575
coll 2907
ts 1048576 1048575
coll 3075

TIMEOUT !
''''''''

[VincentDerk]

If you look at the usage information, you can use

-t [s] set time bound to s seconds

to set a timebound much higher than 100 000. Alternatively, you can change the default value here and recompile.

[Heawen]

Thanks a lot !

[Heawen]

-t [s] set time bound to s seconds

to set a timebound much higher than 100 000. Alternatively, you can change the default value here and recompile.

This two methods above are not working, and it seems that the maximum running time of sharpSAT is still 100000s.
''''
./sharpSAT -t 60 test.cnf

Solving test.cnf
variables (all/used/free): 224/224/0
clauses (all/long/binary/unit): 858/796/60/2

Preprocessing .. DONE
variables (all/used/free): 222/222/0
clauses (all/long/binary/unit): 842/780/62/0
56 16
Maximum cache size: 12767 MB

ts 2097152 2097151
coll 106002

time elapsed: 60.9784s
ts 4194304 4194303
coll 203653

time elapsed: 121.978s
.......
'''''

[VincentDerk]

Try ./sharpSAT -t 1000000000 test.cnf without adding an 's' to the number.

You might also need to consider this #10 (comment)

[Heawen]

Thanks a lot！