Comments (10)
The solution is to:
- Convert the ANF to CNF
- Use a SAT solver like CryptoMiniSat that can find all solutions to a CNF. In cryptominisat, this option is
--maxsol 100000000
- 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.
from bosphorus.
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?
from bosphorus.
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
from bosphorus.
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.
from bosphorus.
Exactly! I'm glad it all works now! Good luck with your project,
Mate
from bosphorus.
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 :)
from bosphorus.
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
from bosphorus.
from bosphorus.
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
from bosphorus.
Ah, thanks, I have just fixed this in d45eea9
Thanks again, that was a good catch!
Mate
from bosphorus.
Related Issues (20)
- Docker build fails due to deprecation of Ubuntu 19.04 HOT 2
- Number of variables HOT 4
- what(): Variable index out of bounds. - with 510 variables and clauses HOT 3
- Evaluating the key research space HOT 6
- terminate called after throwing an instance of 'polybori::PBoRiError'
- Counting the number of solutions after ANF->CNF conversion HOT 7
- We should implement the Linear/Double Partner Strategy, Quadratic Partner Substitution etc ideas by Jovanovic and Kreuzer
- Unexpected behavior on a factored system HOT 3
- Bug in `subsitute` function? HOT 7
- Thoughts on Bosphorus HOT 2
- Bosphorus reports unsat but CryptoMiniSat can solve this SHA-256 CNF HOT 9
- Tests gone missing HOT 4
- How to count the number of solutions to an ANF input?
- Error running: Segmentation fault (core dumped) HOT 2
- cnf simplification problem with double equations HOT 3
- CryptoMiniSat embedded in SageMath can solve these ANFs but Bosphous reports UNSAT HOT 5
- --solvewrite() within Bosphorus is faster than Cryptominisat5 to solve cnf file HOT 7
- If the Bosporus has executable file in Windows system? HOT 1
- It can't convert ANF to CNF. HOT 2
- Multi-thread trigger assertion HOT 5
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from bosphorus.