Wrong result on test case `MaxSAT-keller4-1212.clq.wcnf.sdimacs`

[nianzelee]

The solver produces a wrong result on the test case benchmarks/ssatER/MaxCount/sdimacs/MaxSAT-keller4-1212.clq.wcnf.sdimacs.

The reported probability is 9.755859e-01 with the default configuration, i.e., running

ss benchmarks/ssatER/MaxCount/sdimacs/MaxSAT-keller4-1212.clq.wcnf.sdimacs

However, if the greedy minimization is turned off,

ss -g benchmarks/ssatER/MaxCount/sdimacs/MaxSAT-keller4-1212.clq.wcnf.sdimacs

The reported probability becomes 8.520508e-01.

The discrepancy clearly indicates a bug.

[nianzelee]

@yen-shi , could you please take a look into this issue, if you happen to have some spare time?

[nianzelee]

@perry0513 , could you please comment more on your findings about this bug?

[perry0513]

Hi @nianzelee and @yen-shi !
With the greedy minimization turned on, the solver reports probability 9.755859e-01 with the assignment of the existential variables being
-1 -2 -3 4 -5 -6 ... -12 13 14 15 ... 41 42

However, if the existential assignment
-1 -2 -3 -4 -5 -6 ... -12 13 14 15 ... 41 42
is applied (by adding them as unit clauses to the formula), the solver produces probability 9.833984e-01.

[nianzelee]

The problem with the -g option also arises in the instance er-random-k-CNF/rand-3-30-150-15.57.sdimacs.