CryptoMiniSat embedded in SageMath can solve these ANFs but Bosphous reports UNSAT about bosphorus

[msoos]

Hi, let me reopen this issue. I can't download the file round4rxoodooMess.anf. Can you please send it over or re-attach it? I'd love to see what happened here. Maybe there is a bug. I'm sorry for the very late response :( Can you please send me the file so I can debug?

Thank you in advance, and sorry again for the late response,

Mate

[HuinaLi]

Thanks, Mate. I have re-upload the complete file, please click this link. https://github.com/Lihuina/huina_bosphorus_sagemath/blob/main/huina_bosphorus/bosphorus_code/round4rxoodooMess.anf.
But actually, the problem was gone when I rebuilt the latest Bosphorus, but I don't know whether it is because of my compilation problem or other reasons.
My new log file is attached.
bosphorus_code.zip
round4rxoodooMess.log

[msoos]

Oh, OK, so maybe it was a linking issue. Thanks, I'll keep this in mind, maybe I'll fuzz the system a bit more to see if we can find some issues. Thank you again! And let us know how you think we could improve it :)

Is it faster than the the system in SageMath?

[HuinaLi]

Yes:), it is so cool!

For Sagemath, we takes 107.10 seconds on solving this problem, but for Bosphorus, only takes 13.25 seconds!

Bosphorus has been very useful on some problems I've been working on and has produced good results. Many thanks for your great work!

Huina

[msoos]

Great to hear! 😃 Thanks for the kind feedback!