how to use preprocessor?

[jwaldmann]

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 "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).

[ltentrup]

From the code it seems that the blower binary has to be in the working dir: https://github.com/ltentrup/caqe/blob/643a2e9db61836ca06ac5a773307404fc6fd6ced/src/preprocessor.rs#L85

If I remember correctly, you might need to apply a patch to bloqqer to make it work, too (can't remember the details, though).

Yes, CAQE is parsing the output of bloqqer to provide a valid assignment for the original formula

[jwaldmann]

binary has to be in the working dir:

Thanks. I see. I can change that line to Command::new("bloqqer") then it uses $PATH and it works.

But with caqe --qdo the other branch is used. When I just write

                // Command::new("./bloqqer-qdo")
		Command::new("bloqqer")
                    .arg("--partial-assignment=1")
                    .arg("--keep=1")
                    .arg(&filename)
...

I get

Problem while solving: parse error: Expect `s cnf`, but found `EOF` at 0:0

This is where I need that patched bloqqer? I am guessing that bloqqer-qdo should output something to stderr, because

                   .stdout(f_copy)
                   .stderr(cert_copy)

If I remember correctly, ...

Well .. you were winning qbfeval with this? :-) What is the method for QBF solving that you currently recommend? It seems it's no longer caqe-bloqqer-dqo. But it is quite fast! I have a (graph coloring) qbf instance where depqbf needs 3 minutes, caqe on its own does not get it (> 30 min), but caqe-bloqqer (with the manual work-around I described above) needs 3 seconds only.