This is very cool, especially the automatic proof generation!
That said, I wonder if it would make more sense to use an SMT prover as fallback rather than a SAT solver. The latter requires converting the 32-bit operations into boolean circuits, which might not be the most efficient way to solve the problem considering modern SMT solvers such as Z3 and CVC5 already have built-in efficient support for bit-vectors?
In fact, I believe that's what Alive2 [1] does, which is a similar tool (although with slightly different goals).
I think it might even be possible to make this work for 64-bit vectors with SMT (in most cases).
I think MiniSAT was used precisely because it is dead easy to embed into WebAssembly. I'm aware that Z3 was also ported to WebAssembly, but it will be way larger...
I work in the film industry, not tech, but I like to read hacker news and see what’s new with you programmers.
Just in case nobody else is far enough outside the industry to tell, this is a hilariously nonsensical post title for us ignorant laymen. It sounds like a fake product out of HBO’s Silicon Valley.
Yeah, it was really hard to minimize the title within HN's limit. It comes from the following description in the "how" document (emphases on used words):
> Haroldbot is a tool that checks the equivalence of arithmetic expressions with 32-bit bitvector semantics, running entirely on the client. This task is mostly accomplished by encoding the expression as an array of 32 binary decision diagrams, one for each bit. Since for a given variable ordering a BDD of a boolean function is canonical, this representation offers and easy equivalence test, at the cost of having to build the BDD first.
Not the author, but it is large enough to generalize to any other big bitvectors and small enough to handle. The use of SAT solver of course means that 32-bit is not a hard limit, but humans can't easily look at them.
That said, I wonder if it would make more sense to use an SMT prover as fallback rather than a SAT solver. The latter requires converting the 32-bit operations into boolean circuits, which might not be the most efficient way to solve the problem considering modern SMT solvers such as Z3 and CVC5 already have built-in efficient support for bit-vectors?
In fact, I believe that's what Alive2 [1] does, which is a similar tool (although with slightly different goals).
I think it might even be possible to make this work for 64-bit vectors with SMT (in most cases).
[1] https://github.com/AliveToolkit/alive2