define default value for hashCount == -1

[AL-JiongYang]

Suppose hashCount == k in the procedure of LogSATSearch, we claim to find an answer if we have found threshold solutions when hashCount == k-1 and less than threshold solutions when hashCount == k. However, when hashCount == 0, the status of hashCount == -1 is undefined, resulting in no answer returned and finally outputting UNSAT.

In a normal running when approxmc starts from 0 xor, the case will be avoided, because we have a particular procedure to check if the CNF has threshold solutions as the initial measurement. Therefore, the program goes into LogSATSearch only if there are more than threshold solutions which guarantees the program won't reach the state that query if there are threshold solutions when hashCount == -1 after finding less than threshold solutions when hashCount == 0.

However, when running approxmc starting from greater than 0 xors, it'll jump over the initial measurement which would only run when starting hashCount == 0. Therefore, the guarantee before disappears, and the program will run into the state to query the status of hashCount == -1 which is undefined, however. Finally, it ends up with the error: ApproxMC::SolCount Counter::count(): Assertion `numHashList.size() > 0 && "UNSAT should not be possible"' failed.

You can reproduce the error by the following case: demo.txt when specifying flag: --start t (t >0). Actually, you can reproduce it with any case of less than threshold solutions and starting from greater than 0 xors.

Therefore, propose to define the default value for hashCount == -1 to fix it. Claim that there are always threshold solutions when hashCount == -1.

[AL-JiongYang]

Find that threshold_sols is a mapping from unsigned int to boolean, so -1 may be unreasonable here. Alternatively, we can modify the condition on this line to solve the corner case when hashCount == 0, specifically, to make the condition true when hashCount == 0.

[msoos]

@kuldeepmeel This is the 2nd time there is a bug in this algorithm. You seemed to have proven it correct, but I strongly suggest we re-write it in a way that normal human beings could understand it. I personally don't understand it, and I am afraid it doesn't cover all edge-cases, as per this and previous bug report. Hence this needs to be re-write it in a way that perhaps doesn't conform to the research paper that many people won't read (but only reference), however allows it to be tested, debugged, reasoned about, and eventually, fixed. Can you please take a short at this re-writing?

Thanks,

Mate

[kuldeepmeel]

--start is an advanced operation and not to be used by any non-expert end user. I think there would be corner cases with start @AL-JiongYang is right here but we need to fix the conditions inside "find" on line

[msoos]

Then let's remove that option. It should not be advanced, it should be non-existent. If it cannot be used safely, it should not be present. You will not believe the kind of stuff I have to deal with in CryptoMiniSat when people who don't know what a CNF is want to use some advanced feature and then are getting an error.

-> short version: please remove the option ASAP.

Thanks,

Mate

[msoos]

OK, option removed. No more hassle. Thanks all!

In case you want to re-add it, please:

• [ ] Create a branch with a pull request
• [ ] Create at least 4 test cases
• [ ] Make the test cases pass in GitHub Actions that I set up

Thanks.