msoos
commented
1 year ago Hi,
Different versions will generate different CNFs, but all the CNFs eventually mean the same thing, i.e. if you solve them, the solution would be a solution to the original ANF. The tool can output a solution map that allows you to know how to map the solution from CNF to ANF if you run it with --solmap MAPPING_FILE where MAPPING_FILE will be written by the tool as an output.
Regarding the error you are getting. You seemed to have deleted the bosphorus library, which contains all the relevant information, including the version, so unfortunately I can't tell you which version it was that you used. However, the newest version should be OK. Have you tried? I'd suggest using version:
https://github.com/meelgroup/bosphorus/releases/tag/bosphorus-3.0
And in particular the bosphorus-linux64.gz file -- once ungzipped, it's a static linux executable that will run just fine. Notice that this is a static executable, so you will never have this issue of accidentally deleting the library, since it does not need a library file :)
Good luck,
Mate
zfx-code
When I compiled bosphorus:(cmake ..)
a1880
Dear author. I don't know if it's my problem. I noticed that: the same ANF file use different version bosphorus, will get the different CNF file(including file size and SAT solving speed). For example the executable file: https://github.com/meelgroup/bosphorus/releases/download/bosphorus-3.0/bosphorus-linux64.gz and some version I compiled myself earlier(about 2022.9) get different CNF file. But unfortunately, I lost the history compiled bosphorus file, and now I can't compile successfully. So could you please give me a copy of the newest executable file(like bosphorus-linux64 can run directly, no other dependencies). Because I noticed that my compiled result still need shared libraries: libbosphorus.so.3.0.
Looking forward to your reply! Best wishes to you! --zfx