Infinite loop on grid exploration

[JelminiM]

When running for example python3 main.py input/ver/adder_i6_o4.v -app input/ver/adder_i6_o4.v --grid --subxpat -lpp=2 -ppo=1 --timeout=600 -et=2 -encoding=1 it goes into an infinite loop due to not finding a SAT result in the first iteration, so the value of obtained_wce_exact in xplore.py never gets updated. This behaviour was observed when running on main.

[rodrigo7491]

@MortezaRezaalipour, can you please see if you can reproduce this behaviour on your side?

[MortezaRezaalipour]

Hello,
Yes, I did test that and indeed it's a problem.
I am right now trying to fix it for the sake of the experiments.
My plan is to save the last couple (or more) approximate circuits from the previous iterations, and see if they are all equal. If so, it is most likely true that the exploration is stuck in an infinite loop.

[MortezaRezaalipour]

Sorry, ignore the message above, that is a solution for another bug (which we usually referred to as an infinite loop).
The problem you're referring to, was not causing a problem in the previous iterations (I mean before coming up with the concept of et_partitioning).
We can fix this issue, by checking whether for all current candidates (stored in the current_population list) the maximum number of UNSATs has been reached or not; the max. number of UNSATs equals: lpp * ppo + 1.