[isabelle-dev] AFP: PAPP_Impossibility not terminating

[Makarius]

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