8 ms·

That's very interesting, do you happen to have any toy examples where two model checkers differ?

OscarCunningham 9y ago
The other day I found an error in the Glucose SAT solver, but only when running with one of the options (-rcheck) changed away from its default setting. Glucose produced an alleged satisfying assignment that didn't actually work. So it's possible for mainstream SAT solvers to have errors, but I imagine their default configurations are very thoroughly tested.
- schoen 9y ago
  It's interesting that the SAT solvers haven't put in a check at the very end to confirm that satisfying instances really satisfy the constraints, since that step is of course supposed to be the radically easy one! I guess their authors have had a lot of (usually well-placed) confidence in the solvers' logic and correctness.
  - OscarCunningham 9y ago
    When I told them about it they said that the -rcheck code was inherited from MiniSAT. Since it's also not enabled by default it's understandable that it hadn't been as thoroughly checked as usual. I wouldn't blame them if they just dump it instead of fixing it. But yes it is strange that it doesn't verify its outputs. On the other hand SAT solvers want to be as fast as possible and there shouldn't be a need to do it if the solver is operating correctly.
nanolith 9y ago
In early days of CBMC, it was possible to confuse it and get it to generate incorrect code for MiniSat. This is a representation issue. Those issues have long since been solved. Now CBMC's biggest problem is that of performance, and the developers are diligently working to improve this problem. When Z3 first came out, I built a machine model for a subset of ARMv7 and ran into a few cases that confused Z3, but worked fine in an equivalent MiniSat. However, this was years ago, and it appears -- although I have not verified this -- that the code in Z3 that I narrowed down in preparation to filing a bug report has already been fixed. The machine model has succumbed to bit rot; I abandoned the effort for a model I built on top of Coq. But, it would be interesting to attempt to fire it up again to see if it works now, and if so, use that to perform a binary search to find out when the fix was applied. It shouldn't be hard to create an example where two model checkers differ. Check current bug reports for two model checkers, and build a model that exploits the bug in one model checker but in which the other model checker works. These code bases are complex. They are increasingly infrequent, as the developers working on these model checkers are quite diligent, but subtle errors do exist.

The other day I found an error in the Glucose SAT solver, but only when running with one of the options (-rcheck) changed away from its default setting. Glucose produced an alleged satisfying assignment that didn't actually work. So it's possible for mainstream SAT solvers to have errors, but I imagine their default configurations are very thoroughly tested.

schoen 9y ago
It's interesting that the SAT solvers haven't put in a check at the very end to confirm that satisfying instances really satisfy the constraints, since that step is of course supposed to be the radically easy one! I guess their authors have had a lot of (usually well-placed) confidence in the solvers' logic and correctness.
- OscarCunningham 9y ago
  When I told them about it they said that the -rcheck code was inherited from MiniSAT. Since it's also not enabled by default it's understandable that it hadn't been as thoroughly checked as usual. I wouldn't blame them if they just dump it instead of fixing it. But yes it is strange that it doesn't verify its outputs. On the other hand SAT solvers want to be as fast as possible and there shouldn't be a need to do it if the solver is operating correctly.

nanolith 9y ago

In early days of CBMC, it was possible to confuse it and get it to generate incorrect code for MiniSat. This is a representation issue. Those issues have long since been solved. Now CBMC's biggest problem is that of performance, and the developers are diligently working to improve this problem. When Z3 first came out, I built a machine model for a subset of ARMv7 and ran into a few cases that confused Z3, but worked fine in an equivalent MiniSat. However, this was years ago, and it appears -- although I have not verified this -- that the code in Z3 that I narrowed down in preparation to filing a bug report has already been fixed. The machine model has succumbed to bit rot; I abandoned the effort for a model I built on top of Coq. But, it would be interesting to attempt to fire it up again to see if it works now, and if so, use that to perform a binary search to find out when the fix was applied. It shouldn't be hard to create an example where two model checkers differ. Check current bug reports for two model checkers, and build a model that exploits the bug in one model checker but in which the other model checker works. These code bases are complex. They are increasingly infrequent, as the developers working on these model checkers are quite diligent, but subtle errors do exist.