pysat
pysat copied to clipboard
get_proof() doesn't work for all solvers
Hello Alexey, as requested, I added a new commit in my fork in order to implement a test for the get_proof() function.
At the moment, I left some "print" call in the test for debugging purpose (I'll remove them in a successive commit) because in my opinion the get_proof() function doesn't work for some solvers.
More specifically, here is the result of the test on my laptop:
Here is a short analysis (just a personal opinion):
The problem is:
- Cadical103 and Cadical153 return an empty proof. This seems to be wrong
- maplesat has a problem when prints the variables. Indeed, the variable "3" doesn't exist (I think it should add a "-1" in the function that prints the proof)
- lingeling is probably fine (but there are 2 variables. It could depend on how the solver handles the UNSAT)
- I don't know if the output produced by maplecm is ok (I haven't had the time to go further)
- MinisatGH, Minisat22, Minicard don't support the get_proof() function
Please, check my commit and let me know your ideas.
Thank you. Regards, Marco
Thanks for the update, Marco! This surely requires further attention
- I am not sure why both versions of CaDiCaL report an empty proof. It may be that the formula is a bit too simple I guess, but still...
- All the Maple* solvers should be working fine as well - again, this needs to be analysed. I will have a look when I get a chance.
- Lingeling looks okay to me at first glance.
- MapleCM looks okay to me at first glance.
- MiniSat does not support proof logging - this is known and so it does not need to be tested here. :)
Again, thanks a lot! Alexey