search

sat-group / open-wbo

Open-WBO: state-of-the-art MaxSAT and Pseudo-Boolean solver
Other
72 stars 12 forks source link

Floating point exception for pseudo-Boolean? #6

Open JoD opened 5 years ago

JoD commented 5 years ago

Trying out open-wbo for pseudo-Boolean problems. Got a floating point exception for instance on pastebin when running the command open-wbo_static -formula=1 <instance>. Compiled open-wbo with the default make rs command, with the default makefile.

On a related note, on some other instances, I get Overflow in the Encoding. What are the coefficient / degree limits for open-wbo?

rubengmartins commented 5 years ago

Thanks for the bug report. We are looking into it and will let you know once we fix it.

Regarding your other observation. A Pseudo-Boolean constraint is encoded into CNF using an encoding that is exponential in the worst case. Therefore, if the number of added clauses reach a given threshold, we just report "Overflow in the Encoding". However, this is done because the formula will just become too large and will not be solved by the SAT solver. The latest version of Open-WBO has a linear encoding for Pseudo-Boolean constraints that would avoid this issue at the cost of a worst performance from the SAT solver. We will change the encoding of the Pseudo-Boolean to this method if we estimate the encoding will blow up. Do you have an example of a formula with the message "Overflow in the Encoding"?

JoD commented 5 years ago

I have about 15 instances, I've attached the smallest one (remove .txt extension). smallest.opb.txt

Thanks for looking into this!

JoD commented 5 years ago

(sorry for closing and reopening, pushed the wrong button apparently).

JoD commented 5 years ago

Hey @rubengmartins! Any progress on this issue? I'm evaluating different PB solvers and would definitely like to include Open-WBO in my experiment. Kind regards - Jo