missing method to map back the solution

[ale-depi]

Hi @meelgroup

There is no way to map back the solution found by a SAT solver to the original problem. The tool is very useful because simplifies a lot CNFs but sometimes it is needed the interpretation rather than just the satisfiability.

This could help since CryptoMiniSat do not support anymore the preprocessing as one could see from this.

Remarks.

• In the Arjun README at the end of "How to Build" commands it could be useful an ldconfig.
• Since you are suggesting sudo make install, also ./arjun ... can be just arjun ...
• I see that you are also the developer of ApproxMC. The above suggestion for ldconfig works as well.
• Note that in the section How to use the Python interface, the double ** is get as a Markdown delimiter messing the text.

Thank you for your work.

Alessandro

[msoos]

Thanks for spotting these and opening an issue! I have written a mini-description of what's needed in #8 for mapping back solutions. I have remedied the sudo ldconfig missing in the README. I also did this for ApproxMC. I also fixed the ** :) I'm going to keep open #8, but close this because I believe everything you mentioned has now been addressed except #8. Please do re-open it in case I'm wrong!

Thanks again,

Mate

[msoos]

Please check #8 to see how the new back-mapping works. Please check if it works for you.

Cheers,

Mate