Incorrect count on a specific set of benchmarks

[AL-JiongYang]

I found Ganak always returned the same count 2^50 or 2^60 or 2^70 on a large set of benchmarks. These benchmarks probably originate from the same question according to the filename. I used default values for all options of Ganak 1.0.0.

For example, check out the instance. ApproxMC can enumerate all 1024 solutions but Ganak gives a count of 2^50.

Check out the entire set of benchmarks here.

Actually, the issue may not be due to Ganak. I checked sharpSAT gives the same problematic count of 2^50. Therefore, it's probably an underlying bug in sharpSAT.

[msoos]

Ohhh waaaait now I see! OK, let me see if we managed to fix this with our fix here: https://github.com/meelgroup/ganak/pull/20

[msoos]

Wow, this is a bug, AGAIN.

soos@tiresias:build$ ~/development/sat_solvers/approxmc/build/approxmc or-50-5-1-UC-40.cnf.gz.no_w.cnf  | tail
c strength cache-irred time: 0.00        (0.00      % time)
c strength cache-red time  : 0.00        (0.00      % time)
c avg cls in red 0         : 0.22        
c avg cls in red 1         : 19.44       
c avg cls in red 2         : 44.70       
c Conflicts in UIP         : 965         (74310.80  confl/time_this_thread)
c Max Memory (rss) used    : 6944 kB     
c Total time (this thread) : 0.01        
c [appmc] Number of solutions is: 64*2**4
s mc 1024

soos@tiresias:build$ ./ganak or-50-5-1-UC-40.cnf.gz.no_w.cnf | tail
c cache miss rate 25.8975%
c avg. variable count (stores / hits)   24.5962/6.29637
c 
c 
s SATISFIABLE 
c # solutions 
s mc 1125899906842624
c # END
c 
c time: 1.32242s

WHAT IS GOING ON

[msoos]

ExactMC is correct:

soos@tiresias:build$ ./ExactMC or-50-5-1-UC-40.cnf.gz.no_w.cnf  | tail
Warning[CNF_Formula]: extra clauses beyond stated!
c o time cnf cache: 2.4e-05
c o time kernelize: 0 (block lits: 0; vivi: 0; equ: 0) (max kdepth: 1/1; #kernelizations: 1/1)
c o Total time cost: 0.00019
c o number of (binary) learnt clauses: 0/0
c o number of (useful) sat calls: 0/10
c s type mc
c o The solver log10-estimates a solution of 1024
c s log10-estimate 3.0103
c o Arbitrary precision result is 1024
c s exact arb int 1024

sharpSAT is also incorrect:

soos@tiresias:build$ ~/development/sat_solvers/sharpSAT/build/sharpSAT or-50-5-1-UC-40.cnf.gz.no_w.cnf | tail
cache miss rate 25.8282%
 avg. variable count (stores / hits)    24.7798/6.35764

# solutions 
1125899906842624
# END

time: 12.5186s

[msoos]

Nope, NO INCORRECT COUNT! It's incorrect CNF!

soos@tiresias:build$ grep -v "^c" ../../ganak/build/or-50-5-1-UC-40.cnf.gz.no_w.cnf | wc -l
272

But the header says:

p cnf 100 250

So the header is incorrect. With fixed header, we get:

soos@tiresias:build$ ./ganak or-50-5-1-UC-40.cnf.gz.no_w.cnf-myfix  | tail
c cache miss rate 92.8571%
c avg. variable count (stores / hits)   5.28571/3
c 
c 
s SATISFIABLE 
c # solutions 
s mc 1024
c # END
c 
c time: 0.001807s

and with sharpSAT we get:

soos@tiresias:build$ ./sharpSAT ../../ganak/build/or-50-5-1-UC-40.cnf.gz.no_w.cnf-myfix | tail
cache miss rate 92.8571%
 avg. variable count (stores / hits)    5.28571/3

# solutions 
1024
# END

time: 0.002626s

The actual diff:

soos@tiresias:build$ diff or-50-5-1-UC-40.cnf.gz.no_w.cnf or-50-5-1-UC-40.cnf.gz.no_w.cnf-myfix 
4c4
< p cnf 100 250
---
> p cnf 100 272

We must implement a header check into GANAK!

[msoos]

This part of sharpSAT and GANAK will ignore all clauses beyond claimed in header:

while ((input_file >> c) && clauses_added < nCls) {

[AL-JiongYang]

Wow! That's an in-depth catch! You're right. These CNFs should be verified before solving.

[msoos]

:) I am fixing now. Here is the bugreport to sharpSAT: https://github.com/marcthurley/sharpSAT/issues/14

[AL-JiongYang]

Got it! Thanks for your time and efforts in digging into the bug and fixing it!!!

[msoos]

OK, I got it all fixed now. If anything is off about the header, we exit(-1) with an appropriate bug message.

Thanks so much @AL-JiongYang for this. It was actually quite an interesting bug to fix :)

Mate