4 ms·
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
by 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 agoIt'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 agoWhen 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.