-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Thanks for using CMS! What was the issue using the newest CMS, do you have some examples perhaps? #2
Comments
Hi, I can confirm Leander's observation. Please find the instances here: |
@msoos Thanks for providing CMS! I have never had problems using your solver and CAQE would be quite less competitive without CMS. @vale1410 Thank you for the examples, I do not have instances myself since my experiments in this regard were quite old. I am not sure if there is a way to debug this difference, I call many times into CMS and already small changes (assigned variables, failed assumptions) can have a huge impact on solving performance. |
@msoos I am not opposed to using the official rust bindings. The only reason that I use a fork is that I really want to link statically against CMS and the official bindings only support dynamic linking. |
Hi All, @ltentrup Thanks for using CMS! I'm glad it helped! @vale1410 Thanks! I will debug the difference, it should be easy with such huge differences (e.g. timeout vs 250s). Thanks so much! It's late here now, but I should be done debugging by the end of the week :) @ltentrup As for the rust bindings -- aaah, I see! Do you think it'd make sense to make a static one too? Or that's not possible? I am a bit confused how cargo works. I would be happy to provide a "rust-static/" directory in my source code if that would help. Do you know how to do that? Wanna take a shot at it, perhaps creating a merge request? Maybe it'd need a Cargo.toml in the root dir too? I wouldn't be opposed to that either, actually, if that's the only way :) Let me know, otherwise, I will take a shot at it myself. Currently, the fact that it uses a double-git-setup (i.e. two git directories, one only to do the cargo thing, one the actual code) seems a bit overcomplicated. Or is this standard practice? |
@msoos I think a static-lib variant could be realized using cargo "features" (https://doc.rust-lang.org/cargo/reference/manifest.html#the-features-section) which are basically compile-time flags. Getting rid of the double-git setup is probably incompatible with this change: cargo is pretty picky with respect to the layout of a rust project; the only way to have a Cargo.toml in the root (and the rust sources in a subfolder) is to use cargo workspaces (https://doc.rust-lang.org/book/ch14-03-cargo-workspaces.html) which are incompatible with features. |
I have been a busy bee but I haven't yet figured it out. I'll get there :) They way caqe is using the solver is pretty peculiar. I wonder what's really causing de degradatopm. Most likely having to do with some slight variation on the branching heuristic. I'll look into it deeper soon :) |
Man, I've been chasing my tail with this one. I wonder what's going on. You call the solver so many times, it's a very specific use-case. I will play a bit more, but it's hard :) |
Hi Mate, The QBF instances are found here: If there are any questions, let me know. |
Hi Leander! First of all, amazing work, thanks so much for using CryptoMiniSat! Do you know what was the issue with using the newest? I have tried playing with things, e.g. these repositories:
https://github.com/msoos/cryptominisat-rs
https://github.com/msoos/caqe
You will see they have very minimal changes (diff should work and make thins clear) -- update to newest CMS, adding of set_verbosity() to both cryptominisat-rs and to caqe.rs/dcaqe.rs, setting it to 0. Verbosity 0 in CMS is default but allows me to change it to higher and debug :)
What was the issue, though? I heard from Valentin (Mayer Eichberger) that you decided to use 5.0.1 for the competition because it was faster. Do you have an example where the difference is visible? I'd like to have one where e.g it solves 100s vs 500s or something like that, i.e. where I can really try to debug the difference and fix. It'd be great if I could fix it for you so you could use the latest!
Thanks in advance and thanks so much for the rust binding and using my code, I'm pretty honoured to be honest :)
Cheers!
Mate
The text was updated successfully, but these errors were encountered: