Re:Modern SAT solvers: fast, neat and underused
by debatem1 on Sunday September 29, 2019 @03:35AM
(#21105687)
I've done some program synthesis and equivalence proving with them. It was for sure trivial to express and nontrivial to express in a way that would actually get to a solution. I know of no general shortcuts for avoiding the part where it performs terribly for nonobvious reasons, but then I am not a SAT solver expert.
I've also done a bit of work on concolic execution, which has yielded interesting insights but not useful results. I'll probably write something up for hn if/when it does yield results.
As others have said, my first real use of it was for scheduling problems. It works but isn't really better than a hand rolled naive solver for the scale of problem I was looking at.
They seem to be good for proving obvious things about cryptosystems. It's very interesting to see how quickly block length becomes a security parameter for things like Speck.
Overall I like them and they clearly have potent uses, but... often I find myself shrugging, accepting some constraint, and using the more obvious approach. It may be that I just seldom have to solve a hard enough problem with full generality.
I've also done a bit of work on concolic execution, which has yielded interesting insights but not useful results. I'll probably write something up for hn if/when it does yield results.
As others have said, my first real use of it was for scheduling problems. It works but isn't really better than a hand rolled naive solver for the scale of problem I was looking at.
They seem to be good for proving obvious things about cryptosystems. It's very interesting to see how quickly block length becomes a security parameter for things like Speck.
Overall I like them and they clearly have potent uses, but... often I find myself shrugging, accepting some constraint, and using the more obvious approach. It may be that I just seldom have to solve a hard enough problem with full generality.