search

ltentrup / caqe

CAQE is a solver for quantified Boolean formulas
MIT License
30 stars 6 forks source link

Thanks for using CMS! What was the issue using the newest CMS, do you have some examples perhaps? #2

Open msoos opened 4 years ago

msoos commented 4 years ago

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

vale1410 commented 4 years ago

Hi,

I can confirm Leander's observation. In the following list of instances the new CMS (5.6.8) does worse than 5.0.1.

Please find the instances here:

instances.zip

Screen Shot 2020-01-14 at 6 22 35 pm
ltentrup commented 4 years ago

@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.

ltentrup commented 4 years ago

@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.

msoos commented 4 years ago

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?

ltentrup commented 4 years ago

@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. And there is still another problem: the best way to discover rust libraries is by crates.io and the cryptominisat bindings on crates.io (https://crates.io/crates/cryptominisat) do not seem to be under your control. So even if we change the rust bindings, they will never be visible to the rust community.

msoos commented 4 years ago

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 :)

msoos commented 4 years ago

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 :)

vale1410 commented 4 years ago

Hi Mate, we've found a much better encoding for these games in QBF. Those instances might be better suited to debug the problem. The 4x4 benchmark is probably most suited.

The QBF instances are found here:

https://github.com/vale1410/positional-games-qbf-encoding/releases/download/v1.1-camerareadySAT2020/positional-games-corrective-encodings.zip

If there are any questions, let me know.