On 18/04/2023 11:37, Manuel Eberl wrote:
I do know of that one as well, but it uses some old and rather obscure SAT
solvers (with some custom patches even, I think) and a different proof format
as well (that isn't really used by any modern SAT solvers, I think). Also, as
I recall there was only one suppoerted SAT solver that I managed to find,
compile, and run. And then the approach didn't really scale to my kind of
setting. In earlier versions of the same entry I had SAT instances with 20
million clauses, which was simply too much.
It is clear that this old SAT implementation is not usable anymore.
My question was more in the direction: How much old/obsolete things from
sat.ML are to be expected as clones in your version?
Apparently little or none.
My implementation uses the DRAT format, which seems to be a kind of de-facto
standard in the SAT community nowadays.
I did take some inspiration from the implementation you linked though. I don't
think they had to do any of the low-level fine-tuning with hyps that I had to
do though.
OK, this already provides some clues.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
