Chasing a Bug in a SAT Solver

If you have a large input that triggers a bug and you want to reduce it, it might be worth looking into the Delta Debugging[0] algorithm used by C-Reduce[1] to make minimal test cases for C-like languages. C-Reduce "happens to do a pretty good job reducing the size of programs in languages other than C/C++, such as JavaScript and Rust" so it might work out of the box for you. (Aside: there's also ddSMT for SMT solvers that take SMT-LIB2 input.)

0: https://www.st.cs.uni-saarland.de/dd/

1: https://github.com/csmith-project/creduce

I wrote a CSP solver a while ago. The bugs were alarmingly prone to being incomplete enumeration of solutions. The solver would say "Yep, here's all 2412 solutions to that problem", but there were more solutions out there it missed. I didn't usually know how many solutions there would be so it's hard to distinguish between "all of them" and "95% of them". However that also threw a lot of doubt on when the solver returned unsat - was the problem unsat, or was the solver failing to look in part of the search space?

I didn't find a plausible testing strategy for convincing myself that the last of that class of error was gone and ultimately stopped working on it as a result.

Resolvo (the SAT solver here) has been really good for us. It helped make some conda-forge bots up to 10x faster than the previous C-based solver (libsolv) while being memory safe.

The specific bot tests went from taking 60 minutes to ~6 minutes which is quite remarkable.

i've used drmaciver's property testing library hypothesis to find bugs in c libraries before; it has shrinking. 'doesn't crash' is the easiest property to define, but a bit fiddly to connect to property testing libraries, because you have to spawn a subprocess. in one case i just used fork, _exit, and wait, but in some cases things get ugly then (posix threads guarantee you almost nothing, but fortunately i wasn't using threads)

his 'minithesis' is the best way i've found to learn about implementing property-based testing

sat and smt solvers have gotten astoundingly good, and most of the leading ones are free software. smt-comp shows off new gains every year and has a lineup of the leaders

z3 is a particularly easy smt solver to get started with, in part because of its convenient python binding

a thing sat/smt and property-based testing have in common is that they both solve inverse problems, allowing you to program at a more declarative level

I don't see it mentioned here, but SAT solvers are also good targets for property based testing, providing failure cases for subsequent minimization. There are many properties that can be checked, for example that satisfaction-preserving transformations on an input do not alter the answer the solver returns.

Ah, counting! One of the hardest problems, that's why I suck at probability and stats. Knuths Volume 4

this article has almost zero content on the bug, the debugging, or the fix. I expect more details

Having ended up with a critical bug in the SAT solver I wrote for my undergrad thesis, it really can be a challenge to fix without clear logs. So, always nice to see a little love for contribution through issues and finding minimal ways to reproduce edge cases.

While we do mention how good issue contributions are significant and meaningful, we often forget how there's often more to it than an initial filing, and may overlook the contributions from those that join lengthier issue threads later.

(Oh, and yes, that critical bug did impact the undergrad thesis, but it could be worked around, however meant I couldn't show the full benefits of the solver.)

I thought this was about SAT physics (used in games, etc)