Hard XOR clause violated

meelgroup / gaussmaxhs

GaussMaxHS, a CNF+XOR MaxSAT solver

Other

2 stars 1 forks source link

Hard XOR clause violated #2

Closed vuphan314 closed 2 years ago

vuphan314 commented 2 years ago

Hi @msoos,

GaussMaxHS appears to violate a hard clause:

cat f.wcnf

p wcnf 3 1 4
x 4 1 2 3 0

Output:

gaussmaxhs f.wcnf -verb=0

c MaxHS 3.0.0
xor added to vec:[ 1 2 3 ] (3)
c Solved by Init Bnds.
o 0
s OPTIMUM FOUND
v -1 -2 -3

This may be related to issue #1.

Thank you.

msoos commented 2 years ago

Oh, damn. The -DONLY_TOPLEVEL was enabled in the source code somehow. That caused issues. This has now been fixed. It should be a LOT faster now. Wow, that was a big bug :( Sorry!

msoos commented 2 years ago

Thanks a lot for catching this!