[isabelle-dev] AFP: PAPP_Impossibility not terminating
makarius at sketis.net
Tue Apr 18 11:52:05 CEST 2023
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.
More information about the isabelle-dev