Improbable infinite loop in one_measurement_count

[tanyongkiam]

I'll start by noting that this infinite loop is highly improbable to trigger in practice, so it's debatable whether it needs to be fixed.

I guess it is possible if you are extremely unlucky or the randomness in your C/OS is broken.

Consider the following foo.cnf which has 128 solutions:

p cnf 7 0

In the extremely unlucky case where, for the hashes, we generated 6 empty random XORs (i.e., the random generator returned a '0' bit 6 * 8 = 48 times in a row), then approxmc will go into an infinite loop.

This happens because the following branch of the code does not correctly handle the case where all of the XORs have already been generated but we are still over the threshold:

https://github.com/meelgroup/approxmc/blob/master/src/counter.cpp#L602

To trigger the infinite loop more reliably, set the random cutoff to a low value (so that '0's are much more likely)

@@ -655,7 +663,7 @@ string Counter::gen_rnd_bits(
 {
     string randomBits;
     std::uniform_int_distribution<uint32_t> dist{0, 1000};
-    uint32_t cutoff = 500;
+    uint32_t cutoff = 5;

Then run this bash loop over a few seeds until you hit one that gets into a loop:

for i in {1..1000}
do
  ./approxmc --arjun 0 -s $i foo.cnf
done

A plausible fix is to return a dummy value in the edge case explicitly, such as in the following:

diff --git a/src/counter.cpp b/src/counter.cpp
index f6362ca..b004468 100644
--- a/src/counter.cpp
+++ b/src/counter.cpp
@@ -580,6 +580,14 @@ void Counter::one_measurement_count(
                 return;
             }
 
+            // No further hashes possible
+            if (hashCount == total_max_xors - 1)
+            {
+                numHashList.push_back(total_max_xors);
+                numCountList.push_back(1);
+                return;
+            }
+
             threshold_sols[hashCount] = 0;
             sols_for_hash[hashCount] = num_sols;

[msoos]

This algorithm had to be fixed so many times, I'm not in the mood of fixing it again. I have asked @kuldeepmeel to re-write this algorithm multiple times, because it is very hard to reason about, as it has a hundred edge cases. Unfortunately, every time, he managed to convince me this is somehow a perfect algorithm. And then I, the fuzzer, or others find more bugs.

Unfortunately, your fix looks incorrect to me? If the XORs didn't half the solution space, the original algorithm in the paper is meant to add more XORs, right? That's what the algorithm is supposed to do as far as I understand. It doesn't matter what random numbers we drew before, or how large the sampling set is. Now, my guess is that the algorithm is completely impenetrable to you too, hence this, in my understanding, incorrect fix? I suggest for @kuldeepmeel to look at this, and fix the thing.

I am keeping this open for 4 weeks. After that, I close, because, again, I refuse to fix this algorithm's bugs, as it is an impenetrable algorithm. Sorry for the disappointment. This algorithm as written, is simply not OK, and I refuse to spend a week trying to understand it again just to fix another bug.

[AL-JiongYang]

Thanks for reporting this bug!

I found this bug last year but forgot to commit the fix at that time. Sorry for that! I just submitted my fix in the PR: #41 and explained the reason behind the bug and my fix. My fix should be conceptually the same as @tanyongkiam's.