Florian Lonsing

Thanks for pointing this out! The following call disables techniques that are not yet supported in combination with trace generation: `./depqbf --dep-man=simple --trace=qrp --traditional-qcdcl --no-qbce-dynamic --no-dynamic-nenofex --no-trivial-falsity --no-trivial-truth ./test.qdimacs`

Hi! Thank you very much for your kind feedback! Below, I have attached a C program which enumerates all the possible values of the outermost (i.e., leftmost) existential variables in...

Thanks for pointing this out! The problem seems to be related to producing dynamic libraries on macOS/arm64. If you only want to produce a static library, you can disable the...

Hi, the generation of assignments as shown in my basic example works only if the leftmost quantifier block is existential. It cannot be used to generate assignments to universal variables,...

Yes, exactly, if the outermost quantifier is existential and the formula is satisfiable, then DepQBF can produce assignments to the outermost variables.