Comments (7)
Hi,
You didn't provide the command like you used to generate the CNF from the ANF. And you didn't provide the command line (and the initial output) used to solve with CryptoMiniSat. These are very important. Besides, CryptoMiniSat works slightly differently when running from the command line versus running as a library -- it's optimized to do different things in the two different contexts. However, 24s vs 9h sounds like it's more to do with how you called Bosphorus to generate the CNF from the ANF, rather than how you called CyrptoMiniSat.
Either way, this kind of discrepancy can happen, especially with satisfiable instances. But it's usually not this bad. Please post the exact commands you used to generate the CNF from the ANF, and the exact command you used to solve with CryptoMiniSat, and the first 20 lines out output from CryptoMinSat. Maybe I can then figure it out :) Thanks!
from bosphorus.
Ah, actually, you forgot to give command line for the Bosphorus solving, rather than the CNF writing. Anyway, you only gave one command line, but I need 3 :)
from bosphorus.
Plus please don't forget to give ALL git commit numbers, so I can reproduce. Otherwise, it's impossible to reproduce :S
from bosphorus.
Hi! Mate,
I have now added complete command line and the complete outfile is appended.
operating system: Linux ubuntu18.04.5
On default master branch, and I install git clone https://github.com/meelgroup/bosphorus.git
and successfully compile it, but for supporting multiple threads I add solver.set_num_threads(config.numThreads);
after CMSat::SATSolver solver;
in line 455 in main.cpp.
Bosphorus
nohup /home/user/lhn/bosphorus/build/bosphorus --anfread /home/user/lhn/bosphorus/gimli/6r/6rgimli.anf --anfwrite /home/user/lhn/bosphorus/gimli/6r/6rgimli_out.anf --cnfwrite /home/user/lhn/bosphorus/gimli/6r/6rgimli.cnf --solvewrite /home/user/lhn/bosphorus/gimli/6r/6rgimli_solution -t 1 > /home/user/lhn/bosphorus/gimli/6r/6rgimli_t1.log 2>&1 &
After bosphorus solved, I set the output cnf file(6rgimli.cnf) of Bosphorus as the input cnf file of cryptominisat.
CryptoMiniSat5.8.0
nohup cryptominisat5 6rgimli.cnf > 6rgimli_cryptominisat.log 2>&1 &
6rgimli.zip
6rgimli_cryptominisat.log
Thanks for your reply!
Best regards,
Huina
from bosphorus.
Wait. So you use multi-threaded solving in Bosphorus, but non-multithreaded when you run them separately?
from bosphorus.
Dear Mate,
We use one thread for Bosphorus and cryptominisat5 in this experiment. And we observe that Bosphorus is faster than cryptominisat5 to solve the same .cnf file.
For other complex cryptographic experiments(not this experiment), we set multiple threads for Bosphorus. We mentioned the modification in main.cpp line455 just to help reproduce experiment environment.
from bosphorus.
Hi,
I think the difference may be because CryptoMiniSat behaves slightly differently when called from the command line and when called as a library. The problem is satisfiable, and so randomness plays a HUGE part. For satisfiable problems, you need to run ANY and ALL sat solvers for at least 20 different, randomly generated, similarly hard problems to get an average time to solve. All solvers are EXTREMELY flaky at finding solutions to satisfiable problems. The difference can be 0.1 second vs 1000 second -- with the SAME sat solver, but different random seed. Hence, I strongly suggest not drawing any conclusions at all from a single measurement. Instead, I suggest generating at least 20, but likely better, 100, files of similar complexity (but different e.g. random seed/random key/etc.), and measuring the solving time that way. You will see that the solving time is very similar ON AVERAGE. But ONLY on average. This is true for all sat solvers.
I hope the above helped,
Mate
from bosphorus.
Related Issues (20)
- 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
- 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
- The executable file about the newest bosphorus HOT 4
- cnf to anf conversion makes it unsat HOT 2
- ANF independent set is not translated to CNF indep set HOT 1
- CNF reading does not care about independent set and will lose/create solutions.
- ANF projection set parsing skips file after first comment HOT 1
- Missing end-to-end tests
- Paper link and bib link broken HOT 1
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.