search

meelgroup / bosphorus

Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter
Other
65 stars 18 forks source link

multiple SATs #2

Closed bobcrypt closed 5 years ago

bobcrypt commented 5 years ago

Hi Developers. I'm writing in the hope you may add to bosphorus some option to save all computed SATs in ANF form. It would be useful if the SATs are written in the output file as they are computed and with total computing time till such SAT is appeared. Note that cryptominisat5 provides multiple SATs with option --maxsol. Many thanks in advance, Bob

msoos commented 5 years ago

Why don't you:

1) Get a simplified ANF 2) Convert it to CNF 3) Run it with --maxsol n with --indepvars "...." where you give the original ANF variables from the ANF as the indepvars?

The CNF that is output from the ANF always has a full variable mapping in case you specify --comments 1. Actually, you are probably better off adding a

c ind 1 2 3 4... 0

to the CNF, where 1,2,3, 4 etc. are the original variables from the ANF, as it can be seen in the CNF that is generated once you specify the --comments 1 option.

Please try and get back to us. Please read through the CNF that is generated once the --comments 1 is given, I think it will be clear. Then add the appropriate the c ind.... 0 in the CNF and run with --maxsol N.

Good luck and get back to us!

msoos commented 5 years ago

I am closing as there have been no response for many months.