Comments (5)
Hi,
Thanks! Is this related to this? https://github.com/meelgroup/bosphorus/issues In other words, does that PR fix this bug or it causes this bug? I understand that this needs fixing, but want to understand first how to reproduce.
Cheers,
Mate
from bosphorus.
This issue has nothing to do with pr.
Pr only sets the number of threads of cryptominisat5. Before pr, the number of threads of cryptominisat5 is always 1 regardless of whether the user specifies the thread parameter. In fact, I did not attempt to fix the above assertion failure.
I have uploaded the file r05.cnf for reproducing.
from bosphorus.
Hi,
Sorry for the late response. It was indeed a bug! I fixed it in CryptoMiniSat, here: msoos/cryptominisat@9b4ee6f
If you recompile both CMS and Bosphorus (maybe no need to recompile Bosphorus, depending on your setup), it should now work! I have tested it :)
I would like to thank you for both the perfectly reproducible problem description and your patience. Sorry, lately I've been very busy so I couldn't get to this as soon as I hoped. Nevertheless, about 1 week to fix is probably not too bad. Thanks again for the bug report, it really helped,
Mate
from bosphorus.
Thank you very much, it helps me a lot.
Besides, I have made a pr to set threadNum for cryptominisat in bosphorus, maybe you can consider that.
from bosphorus.
Ah, good point, thanks for the reminder! I merged the PR as well, and cleaned up the code a bit along the way.
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
- --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
- 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.