ApproxMC returning UNSAT for formula with solution
becgabri opened this issue · 3 comments
Hello! I've recently been trying to use ApproxMC for approximate model counting on the number of solutions for a boolean formula and have been relatively impressed with the precision and runtime compared to older techniques. The only issue I've been really running into is calling approxmc on more complicated formulas leads to UNSAT even when the formulas are satisfiable. I have verified this by taking the cnf file that I have been giving as input to approxmc and converting it into assertions to add to z3. z3 will confirm that the same formula is satisfiable even though approxmc says it is not. Is there any reason that ApproxMC would consistently fail to return SAT? I have included one of the cnf files for reference (its been gzipped because of how large it is)
test_file.cnf.gz
Thanks for the error report! Unfortunately, I cannot reproduce this with the file you sent. I get:
$ ./approxmc test_file.cnf
c AppMC SHA revision ab5f9272c9373a261d099d780618dd4153ec1801
c version 8.2.1 20181127
[appmc] using seed: 1
c -- header says num vars: 557722
c -- header says num clauses: 128527
c -- clauses added: 128527
c -- xor clauses added: 0
c -- vars added 557722
[appmc] Sampling set size: 557722
[appmc] Sampling var set contains over 100 variables, not displaying
[appmc] Using start iteration 0
[appmc] Starting up, initial measurement
[appmc] [ 0.00 ] bounded_sol_count looking for 73 solutions -- hashes active: 0
[appmc] Did not find at least threshold+1 (72) we found only 0, exiting AppMC
[appmc] FINISHED AppMC T: 0.07 s
[appmc] Formula was UNSAT
[appmc] Number of solutions is: 0 x 2^0
So the number of solutions displayed is 0 (0 times any number, in this case 1, is still 0). I have also tried with Docker and it also gives the same exact results. So the issue does not trigger with the input you gave. Are you sure this triggers? Can you please give me an input where it triggers? Thanks!
PS: I have fixed the display being ugly with so many sampling variables :) Thanks for this problem, it helped us already!
Note that the problem is indeed unsatisfiable. Lingeling agrees:
$ lingeling test_file.cnf
s UNSATISFIABLE
Furthermore, the problem you gave is UNSAT through proof verification is as well:
$ ./cryptominisat5 test_file.cnf out
$ ./tests/drat-trim/drat-trim test_file.cnf out
c turning on binary mode checking
c parsing input formula with 557722 variables and 128527 clauses
c WARNING: backward mode ignores deletion of (pseudo) unit clause [0] [id 0] 478915 0
c finished parsing, read 9832 bytes from proof file
c UNSAT via unit propagation on the input instance
c 4 of 128527 clauses in core
c 1 of 143 lemmas in core using 4 resolution steps
c 0 RAT lemmas in core; 0 redundant literals in core lemmas
s VERIFIED
c verification time: 0.184 seconds
Please let us know if you have CNF that reproduces the issue :) Thanks!
Thanks for the quick reply! I realized I had a pretty simplistic bug in the code I had written. You are right, the formula is indeed unsatisfiable. Apologies