IDRUP Support

[m-fleury]

Hello,

I have implemented support for IDRUP in Cryptominisat (the paper is available at https://cca.informatik.uni-freiburg.de/papers/FazekasPollittFleuryBiere-MBMV24.pdf). It is a proof format for incremental SAT solving. A checker and a fuzzer are available -- although that version does not support CMS yet (not sure when @arminbiere will update that repo).

The implementation tries to change as little as possible from the structure of the code.

It is not clear to me if you want to include the ipasir_trace_proof function to produce idrup proofs. It is not part of the IPASIR interface, but I do not see any other way to create proofs over the IPASIR interactions before IPASIR2 is out.

[msoos]

Wow. I mean, this is amazing work. I'll write to you over email in a sec :)

[msoos]

Hi,

I have now pushed the new CMS, which has support for XOR proof logging in frat-xor format, and of course it comes with a verified proof checker for frat-xor in Isabelle (in a separate repository, soon to be public), etc. It' s using FRAT, because I find FRAT to be a nicer format, also by Marijn, so it's not like I'm working against the tide :) This is now an accepted paper at CAV, so that's why I had to hold back releasing this early. Took me... a few sleepless nights to do this change. I find it very cool, it can do, together with a proof in Isabelle of the probabilistic approximate model counting of ApproxMC, formally verify approximate model counts. Kinda fun!

Mate

[msoos]

Hi,

I am a bit confused about the change you made -- did you close this PR by accident? Or you think it's not worth the effort? Or since IFRAT is not a thing, it's best to be abandoned? Let me know what you think,

Mate

[m-fleury]

I started working on merging stuff and apparently that closed the PR, sorry for that… But the changes will come eventually

[msoos]

Oh wow, that's amazing! Thank you so much. I can assure you that what you see on GitHub is latest right now. So nothing is held back. Sorry for having to hold back work -- I hate doing that, but I had no choice, CAV is pretty serious about anonymity of authors (perhaps rightfully so -- I'm not complaining, just stating a fact).