caqe

caqe copied to clipboard

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

8

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

msoos

See test case `test_miniscoping_qdo` in `caqe.rs`. Thanks to Alireza Farhadi for reporting this issue

ltentrup

how to use preprocessor?

2

Hi. I am reading https://www.qbflib.org/qbfeval2022_results.php and I conclude that I want `caqe-bloqqer-qdo` (see https://github.com/ekmett/ersatz/pull/90#issuecomment-1973822608) I build the code in this repo here, and I guess that I should ``` (echo...

jwaldmann

How to extract Herbrand functions?

3

The CAQE paper describes a procedure for extracting Herbrand functions for a QBF problem. How do we get the CAQE solver to give us these Herbrand functions?

chrispvm

static linking

2

Do you have a x86-64 static linked version? I tried to compile with: RUSTFLAGS="-C target-feature=+crt-static" cargo build --target x86_64-unknown-linux-gnu --release but it does not work.

jordilevy

how to build dcaqe?

2

I tried to build dcaqe by running "cargo build --release" from the root directory, but it seems like the only executable binary I can get in ./target/release/ is caqe, there's...

hharryyf

Hi, I'm working on an encoding that requires me to 1) find the satisfiability of a QBF, 2) find the assignment of the outermost existential block when the formula is...

hharryyf