Another solution found is not a solution to the ANF

[obhlivoj]

Hi,

I have another problem with Bosphorus (version 5e9d72d) similar to previous one. Given ANF (task2.anf.txt) was processed by Bosphorus to generate CNF (task2.cnf.txt). Cryptominisat solved the CNF, but its outcome (solution2_cnf_false.txt) is not a valid solution of the ANF. I attach the correct solution of the ANF (solution2_anf_right.txt) obtained differently. Furthemore, I am confused that I had to call Cryptominisat separately.
Could you please help?

Thank you
Vojtech

solution2_anf_right.txt
solution2_cnf_false.txt
task2.anf.txt
task2.cnf.txt

[msoos]

I have stated time and time again that you can only use Bosphorus as described, if you want to have a solution that is mapped back to the ANF variables. The variables in the CNF have nothing to do with the variables in the ANF. I have stated this multiple times and it's clear from the way the system works. You must use --solvesat and you can only get one solution that way.

The CNF is output if asked, but its variables DO NOT MAP to the variables that are in the ANF. Please read the code and the research paper, it will explain. I am working on mapping them back, but this code has not been released yet. Perhaps in the next few weeks.

Please only use Bosphorus with --solvesat and do not attempt to use it any other way, as you seem to be not understanding how the system works and no amount of time invested by to try to explain seems to help.

I am now closing this issue. Please do not email me again about the solutions not being correct when in fact they are correct, and have always been. Just use the --solvesat feature. There is absolutely NO other way to get a solution that is mapped back to ANF.

Please don't write to me about this issue again and do not open any issues related to this again. I am now muting this thread.

Mate