ltentrup / caqe Goto Github PK

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

Hi,
first off, thank you for open-sourcing this great solver!
I wanted to compile dCAQE with cargo build --features dcaqe --release but I get an error like this

error[E0433]: failed to resolve: could not find `DCaqeConfig` in `caqe`
 --> src/bin/dcaqe.rs:6:24
  |
6 |     let config = caqe::DCaqeConfig::new(&args);
  |                        ^^^^^^^^^^^ could not find `DCaqeConfig` in `caqe`

For more information about this error, try `rustc --explain E0433`.
error: could not compile `caqe` due to previous error
warning: build failed, waiting for other jobs to finish...

The build without the dcaqe feature works.
Can you provide a fix for this?

Thanks and best regards

Hi!

I was running some benchmarks comparing different DQBF solvers and I noticed that dCAQE in few cases gives a different result than other solvers (SAT instead of UNSAT). So I tried creating a simple example whose satisfiability can be easily checked, for which dCAQE gives wrong result. I found one, see file dcaqebugsimple.dqdimacs in examples.zip. This formula is unsatisfiable, as the first three clauses force variable 7 to be true, another three clauses force 8 to be true and then the last three clauses would need for variables 4 and 5 to depend on 6. However, dCAQE solves this as satisfiable.

Interestingly, even though variable 3 has no impact, if we remove it (see dcaqebugsimpleno3.dqdimacs), dCAQE solves it correctly as unsatisfiable.

Hi.

I am reading https://www.qbflib.org/qbfeval2022_results.php and I conclude that I want caqe-bloqqer-qdo (see ekmett/ersatz#90 (comment))

I build the code in this repo here, and I guess that I should

(echo "p cnf 1 1" && echo "1 0") | caqe --preprocessor=bloqqer  --qdo /dev/stdin

(it works without --preprocessor=bloqqer) but I get

c CommonSolverConfig { filename: Some("/dev/stdin"), verbosity: Warn, statistics: None, specific: CaqeSpecificSolverConfig { options: SolverOptions { abstraction: AbstractionOptions { reuse_b_literals: Some(Partial), reuse_t_literals: Some(Partial), additional_t_literal_constraints: Some(Partial), additional_b_literal_constraints: false, equivalence_constraints: true, universal_reuse_b_literals: true, replace_t_literal_by_variable: true }, expansion: ExpansionOptions { expansion_refinement: Some(Full), dependency_schemes: false, conflict_clause_expansion: true, hamming_heuristics: false }, strong_unsat_refinement: false, refinement_literal_subsumption: false, miniscoping: true, build_conflict_clauses: false, flip_assignments_from_sat_solver: false, skip_levels: None }, qdimacs_output: true, preprocessor: Some(Bloqqer) } }
thread 'main' panicked at src/preprocessor.rs:77:22:
bloqqer failed to start: Os { code: 2, kind: NotFound, message: "No such file or directory" }
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I do have bloqqer in $PATH.

$ bloqqer -v
c [bloqqer] Bloqqer QBF Preprocessor
c [bloqqer] Version 037 8660cb92fefe93bf9a8565b34f956dc918db650c
c [bloqqer] Copyright (C) 2010 by Armin Biere JKU Linz

[EDIT] I can sort-of simulate caqe-bloqqer-qdo with a shell script

f=$(mktemp --suffix=.cnf)
bloqqer $1 $f
caqe --qdo $f
c=$?
rm -f $f
exit $c

but sometimes bloqqer will remove variables? (or solve the formula completely?) and then I am missing their values when processing the answer. I guess that is why caqe needs to supervise the process somehow (see the orginal formula, before preprocessing, and patch the model after solving).

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

Hi, is the caqe 2022QBFEVAL version going to be made available?

I'm interested in using QBF solvers in interactive applications. When I've needed SAT or 2QBF solving in an interactive setting before, it has been convenient that there was both a Python (for prototyping) and JavaScript (for public deployment on the web) interface to the clasp answer-set solver. Rather than suggesting that the caqe project maintain multiple systems of bindings for high-level languages and weird compilation targets, I have a simpler solution.

Add a single new file, caqe/src/bin/libcaqe.rs (or whatever) that exports a single C function with the following signature (and update Cargo.toml to build an associated dylib):

const char* run_caqe(const char* args, const char* input);

It might go something like this. I've only been using Rust for like 3 days, but this advice looks relevant.

use std::ffi::CStr;
use std::os::raw::c_char;
    
#[no_mangle]
pub extern fn run_caqe(args: *const c_char, input: *const c_char) *const c_char {
    // args is whatever you'd have found from main's argv entries, joined by spaces
    // input is whatever you'd have read from the input file
    // return value is pointer to whatever you would have written to stdout
    ... // caller assumes ownership of memory referred to by returned pointer
}

Goals:

• caqe can be run from inside a host process without spawning a new OS process
• filesystem is not touched during execution

Non-goals:

• incremental construction of problems
• structured data API (the embedding code can parse strings just as if it were reading interacting with the solver via stdio)
• be like the inverse of https://github.com/Storyyeller/cryptominisat-rs/blob/master/src/lib.rs (although that would be nice to have in the future)

How does this enable Python usage? Plain Python code can use the builtin ctypes library to dynamically link and call C functions from the native executable. The string-to-string API design here makes the glue code simple while implying some extra overhead for encoding/decoding to strings. Until we've got some example integrations, we don't know if trying to avoid this overhead is relevant. The point is that the language-specific glue code lives outside of the caqe project.

How does this enable JavaScript usage? By compiling Rust to WebAssembly, a browser-compatible library can be built with minimal changes to the codebase. Existing guidance for calling exported C functions will allow calling the one exported function above from plain JavaScript code. The fact that caqe internally uses C++-based CryptoMiniSat somewhat complicates the compile-to-WASM pipeline, but I think the relevant fixes only involve build scripts and not any Rust or C++ changes. Regardless, these build scripts and associated glue logic again live outside the caqe project.

People actually want a QBF solver in JavaScript??? Yes! The core mechanics of the browser-based game Proofdoku involves solving a 2-QBF problem during each main gameplay step. See the discussion of argument.lp in this paper. The game was made before WebAssembly emerged and the C++-to-JavaScript pipeline of the time didn't yield acceptable performance in mobile browsers. In 2021 (and now the solver maintainers provide pre-compiled WASM binaries), I'd happily have run the solver right inside of the browser in the same way I'd like to try using caqe. The problem instances that arise in interactive settings are usually very small, so making sure the solver can run on strange devices (phones, watches, refrigerators, etc.) and without the need to run a central solving service is usually more important than performance in this setting.

Hi,

When I build with cargo build --release (I'm at git commit 356e3da) I get linker errors like the following:

ld: error: undefined symbol: std::__1::cerr

I was able to fix it locally by making the following change in your cryptominisat-rs fork (and updating the cryptominisat dep in Cargo.tml accordingly):

diff --git a/build.rs b/build.rs
index 1310757..f3c93d8 100755
--- a/build.rs
+++ b/build.rs
@@ -30,9 +30,5 @@ fn main() {
     println!("cargo:rustc-link-search=native={}/lib", dst.display());
     println!("cargo:rustc-link-lib=static=cryptominisat5");
 
-    #[cfg(target_os = "macos")]
     println!("cargo:rustc-flags=-l dylib=c++");
-
-    #[cfg(not(target_os = "macos"))]
-    println!("cargo:rustc-flags=-l dylib=stdc++");
 }

Of course that can't be checked in. Sorry, I know almost no rust and I have no idea what the #[ syntax is. If you give me a patch I'm happy to test it, or if you give me a couple of pointers (e.g. the syntax for "target os is X or Y" I'm happy to try to craft a better fix.

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?

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.

I built caqe and was running it, but it terminated with the message ERROR: memory manager can't handle the load. How do I recompile with DLARGEMEM=ON? I tried cargo build -DLARGMEM=ON --release but that was rejected.