search

NTU-ALComLab / ssatABC

Stochastic SAT solver within ABC
Other
5 stars 2 forks source link

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

Open nianzelee opened 4 years ago

nianzelee commented 4 years ago

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 commented 4 years ago

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

nianzelee commented 4 years ago

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

perry0513 commented 4 years ago

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 commented 3 years ago

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