How can one get all the solutions from Bosphorus?

[msoos]

The question has been asked: "given an ANF, how can I find all the solutions to the system given Bosphorus?"

[msoos]

The solution is to:

1. Convert the ANF to CNF
2. Use a SAT solver like CryptoMiniSat that can find all solutions to a CNF. In cryptominisat, this option is --maxsol 100000000
3. Use the solutions

In case the ANF contains helper variables that you don't want the solutions to be over, then do the following. If you want e.g. all the solutions over variables x1,x2, and x4, then add the line:

c ind 1 2 4 0

to the bottom of your CNF. This is called the sampling set (or sometimes the "independent set"). The SAT solver will then only print the solution over these variables, and will only give different solutions over these variables.

[saadislamm]

Thanks for your reply. I am already using cryptominisat for all the solutions as follows:
$ ./cryptominisat5 --maxsol 10000 out.cnf
and first using bosphorus to generate the cnf as follows:
$ ./bosphorus --anfread equations.anf --anfwrite out.anf --cnfwrite out.cnf -s --solvewrite solution

Can't I get all the solutions by just using bosphorus, I mean in the same command?

Also yes, it gives the solutions for the helper variables too but adding "c ind 1 2 3 4 0" at the end of the out.cnf is not working. Am I missing something?

[msoos]

Hi,

Unfortunately, you can't get this purely from Bosphorus at the moment. You need to output to CNF and then use CryptoMiniSat.

For me this system works. Here is an example.

$ cat a2.anf 
x0 + x1 + x2 + x3 + x4 + x5 + x6 + x7

$ ./bosphorus --anfread a2.anf --cnfwrite a2.cnf --comments 1

$ ./cryptominisat5 --maxsol 20000 a2.cnf 
[...]
c Number of solutions found until now:    128
s UNSATISFIABLE

Now, I add the line c ind 1 2 3 to the end of a2.cnf:

$ ./cryptominisat5 --maxsol 20000 a2.cnf 
c Number of solutions found until now:      8
s UNSATISFIABLE

Which seems correct to me. Maybe your ANF is incorrect? Can you please give us the example that doesn't work for you?

Thanks,

Mate

[saadislamm]

I ran your example. It works as you described. I think I misunderstood it first.
What I was expecting was that if I have a system of equations with 64 variables, I will get the solution up til 64 variables as given by bosphorus:

v -0 -1 2 3 -4 -5 6 7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 32 -33 34 35 -36 -37 -38 -39 40 -41 -42 43 -44 -45 46 -47 -48 49 -50 -51 -52 -53 54 -55 -56 -57 -58 59 -60 61 62 63 64

but cryptominisat is giving me something like:

v 1 2 3 4 -5 -6 7 -8 -9 10 11 12 -13 14 15 16 17 18 -19 -20 21 22 -23 24 -25 26 
v 27 28 -29 -30 31 -32 33 34 35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 
v -48 49 -50 51 -52 -53 -54 -55 -56 -57 -58 59 60 61 -62 63 64 65 66 67 68 69 
v 70 71 72 -73 74 75 76 -77 78 79 -80 81 82 83 -84 -85 86 87 88 89 -90 -91 92 
v 93 -94 -95 -96 -97 -98 99 100 101 -102 -103 -104 -105 106 107 108 109 -110 
v -111 -112 113 114 115 116 -117 118 -119 -120 121 122 123 124 -125 -126 127 
v 128 129 130 -131 132 133 -134 -135 -136 -137 -138 -139 -140 141 142 -143 -144 
v -145 -146 147 148 -149 150 -151 -152 -153 154 155 -156 -157 -158 -159 160 161 
v 162 163 164 165 166 -167 168 -169 -170 171 172 173 174 -175 -176 -177 178 179 
v -180 181 182 -183 184 185 -186 -187 -188 -189 190 191 192 193 -194 195 -196 0

So, I have to ignore the solutions after 64th variable. This happens because the anf-to-cnf conversion increases the variables and cryptominisat doesn't know that those are extra variables for which I don't need a solution but bosphorus just prints what I want.
Thank you.

[msoos]

Exactly! I'm glad it all works now! Good luck with your project,

Mate

[msoos]

Hey hey! A very-very new version has been released that can now do what you want, right out of the tool itself! Just add --allsol and it will give you all solutions :) Like this:

docker run --rm -v `pwd`/:/dat/ msoos/bosphorus \
    --anfread /dat/myfile.anf \
    --cnfwrite /dat/myfile.cnf \
    --solve --allsol
[...]
s ANF-SATISFIABLE
v x(0) x(1) x(2) x(3)
s ANF-SATISFIABLE
v x(0) x(1) 1+x(2) 1+x(3)
s ANF-UNSATISFIABLE
c Number of solutions found: 2

Thanks for the issue you raised, it helped us make a better tool :)

[saadislamm]

I really appreciate that. Thank you.
I have never used docker, is there any advantage of using it or should I keep running bosphorus as:

$ ./bosphorus

[msoos]

Glad to hear! As for Docker -- either is fine. Docker can only help you in case you have trouble compiling it. But you seem to be doing fine :)

…

On Mon, Mar 9, 2020, 00:26 saadislamm ***@***.***> wrote: I really appreciate that. Thank you. I have never used docker, is there any advantage of using it or should I keep running bosphorus as: $ ./bosphorus — You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub <#13?email_source=notifications&email_token=AAKF4ONFF7VJGCNNWUZ47ODRGQZRVA5CNFSM4LAQTYTKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEOFEVCI#issuecomment-596265609>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKF4OMPUCX3536FBH6TYVTRGQZRVANCNFSM4LAQTYTA> .

[saadislamm]

After the last update, getting the following error on make -j4:

Copying bosphorus.hpp to /media/Ubuntu/bosphorus/build/include/bosphorus
[ 85%] Built target bosphorus
Copying solvertypesmini.hpp to /media/Ubuntu/bosphorus/build/include/bosphorus
[ 92%] Built target CopyPublicHeaders
[ 92%] Building CXX object src/CMakeFiles/bosphorus-bin.dir/main.cpp.o
/media/Ubuntu/bosphorus/src/main.cpp: In function ‘Bosph::Solution extend_solution(const std::vectorCMSat::lbool&, const std::map<unsigned int, Bosph::VarMap>&, uint32_t)’:
/media/Ubuntu/bosphorus/src/main.cpp:523:18: error: use of ‘s’ before deduction of ‘auto’
for(auto& s: s.sol) {
^
src/CMakeFiles/bosphorus-bin.dir/build.make:62: recipe for target 'src/CMakeFiles/bosphorus-bin.dir/main.cpp.o' failed
make[2]: *** [src/CMakeFiles/bosphorus-bin.dir/main.cpp.o] Error 1
CMakeFiles/Makefile2:195: recipe for target 'src/CMakeFiles/bosphorus-bin.dir/all' failed
make[1]: *** [src/CMakeFiles/bosphorus-bin.dir/all] Error 2
Makefile:127: recipe for target 'all' failed
make: *** [all] Error 2

[msoos]

Ah, thanks, I have just fixed this in d45eea9

Thanks again, that was a good catch!

Mate